Theorem _nf_ex_same ≪ | index | src | ≫

同变元\nf\ex（不可引用）

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

Step	Hyp	Ref	Expression
1		ex_intro_fo	\ex x A \imp \fo x \ex x A
2	1	_nf_comp	\nf x \ex x A

Axiom use

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