Theorem _nf_prov ≪ | index | src | ≫

\nf定理（不可引用）

theorem _nf_prov {x: set} (A: wff x): $ A $ > $ \nf x A $;

Step	Hyp	Ref	Expression
1		introl_imp	\fo x A \imp A \imp \fo x A
2		hyp h	A
3	2	intro_fo	\fo x A
4	1, 3	ax_mp	A \imp \fo x A
5	4	_nf_comp	\nf x A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_10)