Theorem _nf_fo_same ≪ | index | src | ≫

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

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

Step	Hyp	Ref	Expression
1		iff_elimr	(\nf x \fo x A \iff \nf x \neg \ex x \neg A) \imp \nf x \neg \ex x \neg A \imp \nf x \fo x A
2		fo_eqv_negexneg	\fo x A \iff \neg \ex x \neg A
3	2	iff_intro_nf	\nf x \fo x A \iff \nf x \neg \ex x \neg A
4	1, 3	ax_mp	\nf x \neg \ex x \neg A \imp \nf x \fo x A
5		_nf_ex_same	\nf x \ex x \neg A
6	5	_nf_clos_neg	\nf x \neg \ex x \neg A
7	4, 6	ax_mp	\nf x \fo x A

Axiom use

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