Theorem fo_intro_nf ≪ | index | src | ≫

\fo引入(无关)

theorem fo_intro_nf {x: set} (A: wff x): $ \nf x A $ > $ A \imp \fo x A $;

Step	Hyp	Ref	Expression
1		hyp n	\nf x A
2	1	_nf_decomp	A \imp \fo x A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_5, ax_6, ax_7, ax_12)