Theorem fo_elim ≪ | index | src | ≫

\fo消除

theorem fo_elim {x: set} (A: wff x): $ \fo x A \imp A $;

Step	Hyp	Ref	Expression
1		neg_imp_elimrev	(\neg A \imp \neg \fo x A) \imp \fo x A \imp A
2		imp_iff_tran_imp	(\neg A \imp \ex x \neg A) \imp (\ex x \neg A \iff \neg \fo x A) \imp \neg A \imp \neg \fo x A
3		ex_intro	\neg A \imp \ex x \neg A
4	2, 3	ax_mp	(\ex x \neg A \iff \neg \fo x A) \imp \neg A \imp \neg \fo x A
5		exneg_eqv_negfo	\ex x \neg A \iff \neg \fo x A
6	4, 5	ax_mp	\neg A \imp \neg \fo x A
7	1, 6	ax_mp	\fo 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)