Theorem exfo_elim_fo ≪ | index | src | ≫

\ex\fo消除为\fo

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

Step	Hyp	Ref	Expression
1		neg_imp_swap	(\neg \fo x A \imp \fo x \neg \fo x A) \imp \neg \fo x \neg \fo x A \imp \fo x A
2		negfo_intro_fo	\neg \fo x A \imp \fo x \neg \fo x A
3	1, 2	ax_mp	\neg \fo x \neg \fo x A \imp \fo x A
4	3	conv ex	\ex x \fo x A \imp \fo x A

Axiom use

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