Theorem 2eu6 1494

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 1492	. 2 |- ((E!xE.yph /\ E!yE.xph) <-> (E.xE.yph /\ E.zE.wA.xA.y(ph -> (x = z /\ y = w))))
2		19.29r2 1109	. . . 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 1007	. . . . . 6 |- (ph -> A.zph)
4		ax-17 1007	. . . . . 6 |- (ph -> A.wph)
5		hbs1 1371	. . . . . 6 |- ([z / x][w / y]ph -> A.x[z / x][w / y]ph)
6		hbs1 1371	. . . . . . 7 |- ([w / y]ph -> A.y[w / y]ph)
7	6	hbsb 1372	. . . . . 6 |- ([z / x][w / y]ph -> A.y[z / x][w / y]ph)
8		sbequ12 1218	. . . . . . 7 |- (y = w -> (ph <-> [w / y]ph))
9		sbequ12 1218	. . . . . . 7 |- (x = z -> ([w / y]ph <-> [z / x][w / y]ph))
10	8, 9	sylan9bbr 544	. . . . . 6 |- ((x = z /\ y = w) -> (ph <-> [z / x][w / y]ph))
11	3, 4, 5, 7, 10	cbvex2 1355	. . . . 5 |- (E.xE.yph <-> E.zE.w[z / x][w / y]ph)
12		equequ2 1172	. . . . . . . . . 10 |- (z = v -> (x = z <-> x = v))
13		equequ2 1172	. . . . . . . . . 10 |- (w = u -> (y = w <-> y = u))
14	12, 13	bi2anan9 635	. . . . . . . . 9 |- ((z = v /\ w = u) -> ((x = z /\ y = w) <-> (x = v /\ y = u)))
15	14	imbi2d 615	. . . . . . . 8 |- ((z = v /\ w = u) -> ((ph -> (x = z /\ y = w)) <-> (ph -> (x = v /\ y = u))))
16	15	2albidv 1318	. . . . . . 7 |- ((z = v /\ w = u) -> (A.xA.y(ph -> (x = z /\ y = w)) <-> A.xA.y(ph -> (x = v /\ y = u))))
17	16	cbvex2v 1357	. . . . . 6 |- (E.zE.wA.xA.y(ph -> (x = z /\ y = w)) <-> E.vE.uA.xA.y(ph -> (x = v /\ y = u)))
18		ax-17 1007	. . . . . . . 8 |- ((ph -> (x = v /\ y = u)) -> A.z(ph -> (x = v /\ y = u)))
19		ax-17 1007	. . . . . . . 8 |- ((ph -> (x = v /\ y = u)) -> A.w(ph -> (x = v /\ y = u)))
20		ax-17 1007	. . . . . . . . 9 |- ((z = v /\ w = u) -> A.x(z = v /\ w = u))
21	5, 20	hbim 1043	. . . . . . . 8 |- (([z / x][w / y]ph -> (z = v /\ w = u)) -> A.x([z / x][w / y]ph -> (z = v /\ w = u)))
22		ax-17 1007	. . . . . . . . 9 |- ((z = v /\ w = u) -> A.y(z = v /\ w = u))
23	7, 22	hbim 1043	. . . . . . . 8 |- (([z / x][w / y]ph -> (z = v /\ w = u)) -> A.y([z / x][w / y]ph -> (z = v /\ w = u)))
24		equequ1 1171	. . . . . . . . . 10 |- (x = z -> (x = v <-> z = v))
25		equequ1 1171	. . . . . . . . . 10 |- (y = w -> (y = u <-> w = u))
26	24, 25	bi2anan9 635	. . . . . . . . 9 |- ((x = z /\ y = w) -> ((x = v /\ y = u) <-> (z = v /\ w = u)))
27	10, 26	imbi12d 629	. . . . . . . 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 1354	. . . . . . 7 |- (A.xA.y(ph -> (x = v /\ y = u)) <-> A.zA.w([z / x][w / y]ph -> (z = v /\ w = u)))
29	28	2exbii 1088	. . . . . 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 1487	. . . . . 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	3bitri 175	. . . . 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 485	. . . 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 1144	. . . . . . 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 437	. . . . . . 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	bitri 171	. . . . . 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 1088	. . . . 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 1166	. . . . . . . . . . . . 13 |- (z = x <-> x = z)
38		equcom 1166	. . . . . . . . . . . . 13 |- (w = y <-> y = w)
39	37, 38	anbi12i 485	. . . . . . . . . . . 12 |- ((z = x /\ w = y) <-> (x = z /\ y = w))
40	39	imbi2i 183	. . . . . . . . . . 11 |- ((([z / x][w / y]ph /\ ph) -> (z = x /\ w = y)) <-> (([z / x][w / y]ph /\ ph) -> (x = z /\ y = w)))
41		impexp 345	. . . . . . . . . . 11 |- ((([z / x][w / y]ph /\ ph) -> (x = z /\ y = w)) <-> ([z / x][w / y]ph -> (ph -> (x = z /\ y = w))))
42	40, 41	bitri 171	. . . . . . . . . 10 |- ((([z / x][w / y]ph /\ ph) -> (z = x /\ w = y)) <-> ([z / x][w / y]ph -> (ph -> (x = z /\ y = w))))
43	42	2albii 1036	. . . . . . . . 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 1007	. . . . . . . . . 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 1007	. . . . . . . . . 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 1372	. . . . . . . . . . . . 13 |- ([u / w][z / x][w / y]ph -> A.x[u / w][z / x][w / y]ph)
47	46	hbsb 1372	. . . . . . . . . . . 12 |- ([v / z][u / w][z / x][w / y]ph -> A.x[v / z][u / w][z / x][w / y]ph)
48	5, 47	hban 1045	. . . . . . . . . . 11 |- (([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> A.x([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph))
49	48, 20	hbim 1043	. . . . . . . . . 10 |- ((([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> (z = v /\ w = u)) -> A.x(([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> (z = v /\ w = u)))
50	7	hbsb 1372	. . . . . . . . . . . . 13 |- ([u / w][z / x][w / y]ph -> A.y[u / w][z / x][w / y]ph)
51	50	hbsb 1372	. . . . . . . . . . . 12 |- ([v / z][u / w][z / x][w / y]ph -> A.y[v / z][u / w][z / x][w / y]ph)
52	7, 51	hban 1045	. . . . . . . . . . 11 |- (([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> A.y([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph))
53	52, 22	hbim 1043	. . . . . . . . . 10 |- ((([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> (z = v /\ w = u)) -> A.y(([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> (z = v /\ w = u)))
54		sbequ12 1218	. . . . . . . . . . . . . 14 |- (y = u -> (ph <-> [u / y]ph))
55		sbequ12 1218	. . . . . . . . . . . . . 14 |- (x = v -> ([u / y]ph <-> [v / x][u / y]ph))
56	54, 55	sylan9bbr 544	. . . . . . . . . . . . 13 |- ((x = v /\ y = u) -> (ph <-> [v / x][u / y]ph))
57		ax-17 1007	. . . . . . . . . . . . . . 15 |- ([u / w][w / y]ph -> A.z[u / w][w / y]ph)
58	57	sbco2 1293	. . . . . . . . . . . . . 14 |- ([v / z][z / x][u / w][w / y]ph <-> [v / x][u / w][w / y]ph)
59		sbcom2 1373	. . . . . . . . . . . . . . 15 |- ([z / x][u / w][w / y]ph <-> [u / w][z / x][w / y]ph)
60	59	sbbii 1211	. . . . . . . . . . . . . 14 |- ([v / z][z / x][u / w][w / y]ph <-> [v / z][u / w][z / x][w / y]ph)
61	4	sbco2 1293	. . . . . . . . . . . . . . 15 |- ([u / w][w / y]ph <-> [u / y]ph)
62	61	sbbii 1211	. . . . . . . . . . . . . 14 |- ([v / x][u / w][w / y]ph <-> [v / x][u / y]ph)
63	58, 60, 62	3bitr3ri 180	. . . . . . . . . . . . 13 |- ([v / x][u / y]ph <-> [v / z][u / w][z / x][w / y]ph)
64	56, 63	syl6bb 539	. . . . . . . . . . . 12 |- ((x = v /\ y = u) -> (ph <-> [v / z][u / w][z / x][w / y]ph))
65	64	anbi2d 619	. . . . . . . . . . 11 |- ((x = v /\ y = u) -> (([z / x][w / y]ph /\ ph) <-> ([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph)))
66		equequ2 1172	. . . . . . . . . . . 12 |- (x = v -> (z = x <-> z = v))
67		equequ2 1172	. . . . . . . . . . . 12 |- (y = u -> (w = y <-> w = u))
68	66, 67	bi2anan9 635	. . . . . . . . . . 11 |- ((x = v /\ y = u) -> ((z = x /\ w = y) <-> (z = v /\ w = u)))
69	65, 68	imbi12d 629	. . . . . . . . . 10 |- ((x = v /\ y = u) -> ((([z / x][w / y]ph /\ ph) -> (z = x /\ w = y)) <-> (([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> (z = v /\ w = u))))
70	44, 45, 49, 53, 69	cbval2 1354	. . . . . . . . 9 |- (A.xA.y(([z / x][w / y]ph /\ ph) -> (z = x /\ w = y)) <-> A.vA.u(([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> (z = v /\ w = u)))
71	5, 7	19.21-2 1093	. . . . . . . . 9 |- (A.xA.y([z / x][w / y]ph -> (ph -> (x = z /\ y = w))) <-> ([z / x][w / y]ph -> A.xA.y(ph -> (x = z /\ y = w))))
72	43, 70, 71	3bitr3i 179	. . . . . . . 8 |- (A.vA.u(([z / x][w / y]ph /\ [v / z][u / w][z / x][w / y]ph) -> (z = v /\ w = u)) <-> ([z / x][w / y]ph -> A.xA.y(ph -> (x = z /\ y = w))))
73	72	anbi2i 483	. . . . . . 7 |- (([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))) <-> ([z / x][w / y]ph /\ ([z / x][w / y]ph -> A.xA.y(ph -> (x = z /\ y = w)))))
74		abai 482	. . . . . . 7 |- (([z / x][w / y]ph /\ A.xA.y(ph -> (x = z /\ y = w))) <-> ([z / x][w / y]ph /\ ([z / x][w / y]ph -> A.xA.y(ph -> (x = z /\ y = w)))))
75		2sb6 1375	. . . . . . . 8 |- ([z / x][w / y]ph <-> A.xA.y((x = z /\ y = w) -> ph))
76	75	anbi1i 484	. . . . . . 7 |- (([z / x][w / y]ph /\ A.xA.y(ph -> (x = z /\ y = w))) <-> (A.xA.y((x = z /\ y = w) -> ph) /\ A.xA.y(ph -> (x = z /\ y = w))))
77	73, 74, 76	3bitr2i 177	. . . . . 6 |- (([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))) <-> (A.xA.y((x = z /\ y = w) -> ph) /\ A.xA.y(ph -> (x = z /\ y = w))))
78	77	2exbii 1088	. . . . 5 |- (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))) <-> E.zE.w(A.xA.y((x = z /\ y = w) -> ph) /\ A.xA.y(ph -> (x = z /\ y = w))))
79	36, 78	bitr4i 174	. . . 4 |- (E.zE.wA.xA.y(ph <-> (x = z /\ y = w)) <-> 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))))
80	2, 32, 79	3imtr4i 217	. . 3 |- ((E.xE.yph /\ E.zE.wA.xA.y(ph -> (x = z /\ y = w))) -> E.zE.wA.xA.y(ph <-> (x = z /\ y = w)))
81		bi2 147	. . . . . . 7 |- ((ph <-> (x = z /\ y = w)) -> ((x = z /\ y = w) -> ph))
82	81	19.20i2 1029	. . . . . 6 |- (A.xA.y(ph <-> (x = z /\ y = w)) -> A.xA.y((x = z /\ y = w) -> ph))
83	82	19.22i2 1077	. . . . 5 |- (E.zE.wA.xA.y(ph <-> (x = z /\ y = w)) -> E.zE.wA.xA.y((x = z /\ y = w) -> ph))
84		2exsb 1390	. . . . 5 |- (E.xE.yph <-> E.zE.wA.xA.y((x = z /\ y = w) -> ph))
85	83, 84	sylibr 198	. . . 4 |- (E.zE.wA.xA.y(ph <-> (x = z /\ y = w)) -> E.xE.yph)
86		bi1 146	. . . . . 6 |- ((ph <-> (x = z /\ y = w)) -> (ph -> (x = z /\ y = w)))
87	86	19.20i2 1029	. . . . 5 |- (A.xA.y(ph <-> (x = z /\ y = w)) -> A.xA.y(ph -> (x = z /\ y = w)))
88	87	19.22i2 1077	. . . 4 |- (E.zE.wA.xA.y(ph <-> (x = z /\ y = w)) -> E.zE.wA.xA.y(ph -> (x = z /\ y = w)))
89	85, 88	jca 286	. . 3 |- (E.zE.wA.xA.y(ph <-> (x = z /\ y = w)) -> (E.xE.yph /\ E.zE.wA.xA.y(ph -> (x = z /\ y = w))))
90	80, 89	impbii 155	. 2 |- ((E.xE.yph /\ E.zE.wA.xA.y(ph -> (x = z /\ y = w))) <-> E.zE.wA.xA.y(ph <-> (x = z /\ y = w)))
91	1, 90	bitri 171	1 |- ((E!xE.yph /\ E!yE.xph) <-> E.zE.wA.xA.y(ph <-> (x = z /\ y = w)))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221  A.wal 990   = wceq 992  E.wex 1016  E!weu 1419

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421

Copyright terms: Public domain