Theorem 2eu6 1452

Description: Two equivalent expressions for double existential uniqueness.

Assertion

Ref	Expression
2eu6	|- ((E!xE.yph /\ E!yE.xph) <-> E.zE.wA.xA.y(ph <-> (x = z /\ y = w)))

Distinct variable groups:   x,y,z,w   ph,z,w

Proof of Theorem 2eu6

Step	Hyp	Ref	Expression
1		2eu4 1450	. 2 |- ((E!xE.yph /\ E!yE.xph) <-> (E.xE.yph /\ E.zE.wA.xA.y(ph -> (x = z /\ y = w))))
2		19.29r2 1071	. . . 4 |- ((E.zE.w[z / x][w / y]ph /\ A.zA.wA.vA.u(([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> (z = v /\ w = u))) -> E.zE.w([z / x][w / y]ph /\ A.vA.u(([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> (z = v /\ w = u))))
3		ax-17 969	. . . . . 6 |- (ph -> A.zph)
4		ax-17 969	. . . . . 6 |- (ph -> A.wph)
5		hbs1 1330	. . . . . 6 |- ([z / x][w / y]ph -> A.x[z / x][w / y]ph)
6		hbs1 1330	. . . . . . 7 |- ([w / y]ph -> A.y[w / y]ph)
7	6	hbsb 1331	. . . . . 6 |- ([z / x][w / y]ph -> A.y[z / x][w / y]ph)
8		sbequ12 1179	. . . . . . 7 |- (y = w -> (ph <-> [w / y]ph))
9		sbequ12 1179	. . . . . . 7 |- (x = z -> ([w / y]ph <-> [z / x][w / y]ph))
10	8, 9	sylan9bbr 540	. . . . . 6 |- ((x = z /\ y = w) -> (ph <-> [z / x][w / y]ph))
11	3, 4, 5, 7, 10	cbvex2 1315	. . . . 5 |- (E.xE.yph <-> E.zE.w[z / x][w / y]ph)
12		equequ2 1133	. . . . . . . . . 10 |- (z = v -> (x = z <-> x = v))
13		equequ2 1133	. . . . . . . . . 10 |- (w = u -> (y = w <-> y = u))
14	12, 13	bi2anan9 631	. . . . . . . . 9 |- ((z = v /\ w = u) -> ((x = z /\ y = w) <-> (x = v /\ y = u)))
15	14	imbi2d 611	. . . . . . . 8 |- ((z = v /\ w = u) -> ((ph -> (x = z /\ y = w)) <-> (ph -> (x = v /\ y = u))))
16	15	2albidv 1278	. . . . . . 7 |- ((z = v /\ w = u) -> (A.xA.y(ph -> (x = z /\ y = w)) <-> A.xA.y(ph -> (x = v /\ y = u))))
17	16	cbvex2v 1317	. . . . . 6 |- (E.zE.wA.xA.y(ph -> (x = z /\ y = w)) <-> E.vE.uA.xA.y(ph -> (x = v /\ y = u)))
18		ax-17 969	. . . . . . . 8 |- ((ph -> (x = v /\ y = u)) -> A.z(ph -> (x = v /\ y = u)))
19		ax-17 969	. . . . . . . 8 |- ((ph -> (x = v /\ y = u)) -> A.w(ph -> (x = v /\ y = u)))
20		ax-17 969	. . . . . . . . 9 |- ((z = v /\ w = u) -> A.x(z = v /\ w = u))
21	5, 20	hbim 1005	. . . . . . . 8 |- (([z / x][w / y]ph -> (z = v /\ w = u)) -> A.x([z / x][w / y]ph -> (z = v /\ w = u)))
22		ax-17 969	. . . . . . . . 9 |- ((z = v /\ w = u) -> A.y(z = v /\ w = u))
23	7, 22	hbim 1005	. . . . . . . 8 |- (([z / x][w / y]ph -> (z = v /\ w = u)) -> A.y([z / x][w / y]ph -> (z = v /\ w = u)))
24		equequ1 1132	. . . . . . . . . 10 |- (x = z -> (x = v <-> z = v))
25		equequ1 1132	. . . . . . . . . 10 |- (y = w -> (y = u <-> w = u))
26	24, 25	bi2anan9 631	. . . . . . . . 9 |- ((x = z /\ y = w) -> ((x = v /\ y = u) <-> (z = v /\ w = u)))
27	10, 26	imbi12d 625	. . . . . . . 8 |- ((x = z /\ y = w) -> ((ph -> (x = v /\ y = u)) <-> ([z / x][w / y]ph -> (z = v /\ w = u))))
28	18, 19, 21, 23, 27	cbval2 1314	. . . . . . 7 |- (A.xA.y(ph -> (x = v /\ y = u)) <-> A.zA.w([z / x][w / y]ph -> (z = v /\ w = u)))
29	28	2exbii 1050	. . . . . 6 |- (E.vE.uA.xA.y(ph -> (x = v /\ y = u)) <-> E.vE.uA.zA.w([z / x][w / y]ph -> (z = v /\ w = u)))
30		2mo 1445	. . . . . 6 |- (E.vE.uA.zA.w([z / x][w / y]ph -> (z = v /\ w = u)) <-> A.zA.wA.vA.u(([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> (z = v /\ w = u)))
31	17, 29, 30	3bitr 177	. . . . 5 |- (E.zE.wA.xA.y(ph -> (x = z /\ y = w)) <-> A.zA.wA.vA.u(([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> (z = v /\ w = u)))
32	11, 31	anbi12i 482	. . . 4 |- ((E.xE.yph /\ E.zE.wA.xA.y(ph -> (x = z /\ y = w))) <-> (E.zE.w[z / x][w / y]ph /\ A.zA.wA.vA.u(([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> (z = v /\ w = u))))
33		2albi 1106	. . . . . . 7 |- (A.xA.y(ph <-> (x = z /\ y = w)) <-> (A.xA.y(ph -> (x = z /\ y = w)) /\ A.xA.y((x = z /\ y = w) -> ph)))
34		ancom 435	. . . . . . 7 |- ((A.xA.y(ph -> (x = z /\ y = w)) /\ A.xA.y((x = z /\ y = w) -> ph)) <-> (A.xA.y((x = z /\ y = w) -> ph) /\ A.xA.y(ph -> (x = z /\ y = w))))
35	33, 34	bitr 173	. . . . . 6 |- (A.xA.y(ph <-> (x = z /\ y = w)) <-> (A.xA.y((x = z /\ y = w) -> ph) /\ A.xA.y(ph -> (x = z /\ y = w))))
36	35	2exbii 1050	. . . . 5 |- (E.zE.wA.xA.y(ph <-> (x = z /\ y = w)) <-> E.zE.w(A.xA.y((x = z /\ y = w) -> ph) /\ A.xA.y(ph -> (x = z /\ y = w))))
37		equcom 1127	. . . . . . . . . . . . 13 |- (z = x <-> x = z)
38		equcom 1127	. . . . . . . . . . . . 13 |- (w = y <-> y = w)
39	37, 38	anbi12i 482	. . . . . . . . . . . 12 |- ((z = x /\ w = y) <-> (x = z /\ y = w))
40	39	imbi2i 185	. . . . . . . . . . 11 |- ((([z / x][w / y]ph /\ ph) -> (z = x /\ w = y)) <-> (([z / x][w / y]ph /\ ph) -> (x = z /\ y = w)))
41		impexp 347	. . . . . . . . . . 11 |- ((([z / x][w / y]ph /\ ph) -> (x = z /\ y = w)) <-> ([z / x][w / y]ph -> (ph -> (x = z /\ y = w))))
42	40, 41	bitr 173	. . . . . . . . . 10 |- ((([z / x][w / y]ph /\ ph) -> (z = x /\ w = y)) <-> ([z / x][w / y]ph -> (ph -> (x = z /\ y = w))))
43	42	2albii 998	. . . . . . . . 9 |- (A.xA.y(([z / x][w / y]ph /\ ph) -> (z = x /\ w = y)) <-> A.xA.y([z / x][w / y]ph -> (ph -> (x = z /\ y = w))))
44		ax-17 969	. . . . . . . . . 10 |- ((([z / x][w / y]ph /\ ph) -> (z = x /\ w = y)) -> A.v(([z / x][w / y]ph /\ ph) -> (z = x /\ w = y)))
45		ax-17 969	. . . . . . . . . 10 |- ((([z / x][w / y]ph /\ ph) -> (z = x /\ w = y)) -> A.u(([z / x][w / y]ph /\ ph) -> (z = x /\ w = y)))
46	5	hbsb 1331	. . . . . . . . . . . . 13 |- ([u / w][z / x][w / y]ph -> A.x[u / w][z / x][w / y]ph)
47	46	hbsb 1331	. . . . . . . . . . . 12