Theorem e2ebindALT

Description: Absorption of an existential quantifier of a double existential quantifier of non-distinct variables. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in e2ebindVD . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	e2ebindALT	$$⊢\forall xx=y\to \left(\exists x\exists y\phi \leftrightarrow \exists y\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		axc11n	$$⊢\forall xx=y\to \forall yy=x$$
2		nfe1	$$⊢Ⅎy\exists y\phi$$
3	2	19.9	$$⊢\exists y\exists y\phi \leftrightarrow \exists y\phi$$
4		excom	$$⊢\exists y\exists x\phi \leftrightarrow \exists x\exists y\phi$$
5		nfa1	$$⊢Ⅎy\forall yy=x$$
6		id	$$⊢\forall yy=x\to \forall yy=x$$
7		biid	$$⊢\phi \leftrightarrow \phi$$
8	7	a1i	$$⊢\forall yy=x\to \left(\phi \leftrightarrow \phi \right)$$
9	8	drex1	$$⊢\forall yy=x\to \left(\exists y\phi \leftrightarrow \exists x\phi \right)$$
10	6 9	syl	$$⊢\forall yy=x\to \left(\exists y\phi \leftrightarrow \exists x\phi \right)$$
11	5 10	alrimi	$$⊢\forall yy=x\to \forall y\left(\exists y\phi \leftrightarrow \exists x\phi \right)$$
12		exbi	$$⊢\forall y\left(\exists y\phi \leftrightarrow \exists x\phi \right)\to \left(\exists y\exists y\phi \leftrightarrow \exists y\exists x\phi \right)$$
13	11 12	syl	$$⊢\forall yy=x\to \left(\exists y\exists y\phi \leftrightarrow \exists y\exists x\phi \right)$$
14		bitr	$$⊢\left(\left(\exists y\exists y\phi \leftrightarrow \exists y\exists x\phi \right)\wedge \left(\exists y\exists x\phi \leftrightarrow \exists x\exists y\phi \right)\right)\to \left(\exists y\exists y\phi \leftrightarrow \exists x\exists y\phi \right)$$
15	14	ex	$$⊢\left(\exists y\exists y\phi \leftrightarrow \exists y\exists x\phi \right)\to \left(\left(\exists y\exists x\phi \leftrightarrow \exists x\exists y\phi \right)\to \left(\exists y\exists y\phi \leftrightarrow \exists x\exists y\phi \right)\right)$$
16	15	impcom	$$⊢\left(\left(\exists y\exists x\phi \leftrightarrow \exists x\exists y\phi \right)\wedge \left(\exists y\exists y\phi \leftrightarrow \exists y\exists x\phi \right)\right)\to \left(\exists y\exists y\phi \leftrightarrow \exists x\exists y\phi \right)$$
17	4 13 16	sylancr	$$⊢\forall yy=x\to \left(\exists y\exists y\phi \leftrightarrow \exists x\exists y\phi \right)$$
18		bitr3	$$⊢\left(\exists y\exists y\phi \leftrightarrow \exists x\exists y\phi \right)\to \left(\left(\exists y\exists y\phi \leftrightarrow \exists y\phi \right)\to \left(\exists x\exists y\phi \leftrightarrow \exists y\phi \right)\right)$$
19	18	impcom	$$⊢\left(\left(\exists y\exists y\phi \leftrightarrow \exists y\phi \right)\wedge \left(\exists y\exists y\phi \leftrightarrow \exists x\exists y\phi \right)\right)\to \left(\exists x\exists y\phi \leftrightarrow \exists y\phi \right)$$
20	3 17 19	sylancr	$$⊢\forall yy=x\to \left(\exists x\exists y\phi \leftrightarrow \exists y\phi \right)$$
21	1 20	syl	$$⊢\forall xx=y\to \left(\exists x\exists y\phi \leftrightarrow \exists y\phi \right)$$