Theorem 2moswap

Description: A condition allowing to swap an existential quantifier and at at-most-one quantifier. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker 2moswapv when possible. (Contributed by NM, 10-Apr-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	2moswap	$$⊢\forall x{\exists }^{*}y\phi \to \left({\exists }^{*}x\exists y\phi \to {\exists }^{*}y\exists x\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfe1	$$⊢Ⅎy\exists y\phi$$
2	1	moexex	$$⊢\left({\exists }^{*}x\exists y\phi \wedge \forall x{\exists }^{*}y\phi \right)\to {\exists }^{*}y\exists x\left(\exists y\phi \wedge \phi \right)$$
3	2	expcom	$$⊢\forall x{\exists }^{*}y\phi \to \left({\exists }^{*}x\exists y\phi \to {\exists }^{*}y\exists x\left(\exists y\phi \wedge \phi \right)\right)$$
4		19.8a	$$⊢\phi \to \exists y\phi$$
5	4	pm4.71ri	$$⊢\phi \leftrightarrow \left(\exists y\phi \wedge \phi \right)$$
6	5	exbii	$$⊢\exists x\phi \leftrightarrow \exists x\left(\exists y\phi \wedge \phi \right)$$
7	6	mobii	$$⊢{\exists }^{*}y\exists x\phi \leftrightarrow {\exists }^{*}y\exists x\left(\exists y\phi \wedge \phi \right)$$
8	3 7	syl6ibr	$$⊢\forall x{\exists }^{*}y\phi \to \left({\exists }^{*}x\exists y\phi \to {\exists }^{*}y\exists x\phi \right)$$