Theorem _nf_abs ≪ | index | src | ≫

\nf不出现（不可引用）

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

Step	Hyp	Ref	Expression
1		imp_tran	(\ex x A \imp A) \imp (A \imp \fo x A) \imp \ex x A \imp \fo x A
2		ex_elim_abs	\ex x A \imp A
3	1, 2	ax_mp	(A \imp \fo x A) \imp \ex x A \imp \fo x A
4		fo_intro_abs	A \imp \fo x A
5	3, 4	ax_mp	\ex x A \imp \fo x A
6	5	conv nf	\nf x A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_5)