Theorem _nf_clos_fo_difvar ≪ | index | src | ≫

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

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

Step	Hyp	Ref	Expression
1		imp_tran	(\fo y A \imp \fo y \fo x A) \imp (\fo y \fo x A \imp \fo x \fo y A) \imp \fo y A \imp \fo x \fo y A
2		hyp h	\nf x A
3	2	_nf_decomp	A \imp \fo x A
4	3	imp_intro_fo	\fo y A \imp \fo y \fo x A
5	1, 4	ax_mp	(\fo y \fo x A \imp \fo x \fo y A) \imp \fo y A \imp \fo x \fo y A
6		fo_swap	\fo y \fo x A \imp \fo x \fo y A
7	5, 6	ax_mp	\fo y A \imp \fo x \fo y A
8	7	_nf_comp	\nf x \fo 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)