Theorem ex_swap ≪ | index | src | ≫

\ex交换

theorem ex_swap {x y: set} (A: wff x y): $ \ex x \ex y A \imp \ex y \ex x A $;

Step	Hyp	Ref	Expression
1		iff_decomp	(\ex x \ex y A \iff \ex y \ex x A) \imp \ex x \ex y A \imp \ex y \ex x A
2		ex_perm	\ex x \ex y A \iff \ex y \ex x A
3	1, 2	ax_mp	\ex x \ex y A \imp \ex y \ex x A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_11)