Theorem fo_to_ex ≪ | index | src | ≫

\fo变成\ex

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

Step	Hyp	Ref	Expression
1		iff_eliml	(\ex x (A \imp A) \iff \fo x A \imp \ex x A) \imp \ex x (A \imp A) \imp \fo x A \imp \ex x A
2		ex_imp_distto_fo_ex	\ex x (A \imp A) \iff \fo x A \imp \ex x A
3	1, 2	ax_mp	\ex x (A \imp A) \imp \fo x A \imp \ex x A
4		ex_intro	(A \imp A) \imp \ex x (A \imp A)
5		imp_refl	A \imp A
6	4, 5	ax_mp	\ex x (A \imp A)
7	3, 6	ax_mp	\fo x A \imp \ex x A

Axiom use

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