Theorem ex_alloc_abs ≪ | index | src | ≫

\ex指配(不出现)

theorem ex_alloc_abs (A: wff) {x: set}: $ A \iff \ex x A $;

Step	Hyp	Ref	Expression
1		iff_comp	(A \imp \ex x A) \imp (\ex x A \imp A) \imp (A \iff \ex x A)
2		ex_intro	A \imp \ex x A
3	1, 2	ax_mp	(\ex x A \imp A) \imp (A \iff \ex x A)
4		ex_elim_abs	\ex x A \imp A
5	3, 4	ax_mp	A \iff \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)