Theorem ex_elim_nf ≪ | index | src | ≫

\ex消除(无关)

theorem ex_elim_nf {x: set} (A: wff x): $ \nf x A $ > $ \ex x A \imp A $;

Step	Hyp	Ref	Expression
1		neg_imp_swap	(\neg A \imp \fo x \neg A) \imp \neg \fo x \neg A \imp A
2		hyp n	\nf x A
3	2	_nf_clos_neg	\nf x \neg A
4	3	_nf_decomp	\neg A \imp \fo x \neg A
5	1, 4	ax_mp	\neg \fo x \neg A \imp A
6	5	conv ex	\ex x A \imp A

Axiom use

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