Theorem _nf_clos_nf_difvar ≪ | index | src | ≫

\nf闭包\nf不同变元（不可引用）

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

Step	Hyp	Ref	Expression
1		hyp h	\nf x A
2	1	_nf_clos_ex_difvar	\nf x \ex y A
3	1	_nf_clos_fo_difvar	\nf x \fo y A
4	2, 3	_nf_clos_imp	\nf x (\ex y A \imp \fo y A)
5	4	conv nf	\nf x \nf y A

Axiom use

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