Theorem 2reu5lem3 3044

Description: Lemma for 2reu5 3045. This lemma is interesting in its own right, showing that existential restriction in the last conjunct (the "at most one" part) is optional; compare rmo2 3132. (Contributed by Alexander van der Vekens, 17-Jun-2017.)

Assertion

Ref	Expression
2reu5lem3	|- ((E!x e. A E!y e. B ph /\ A.x e. A E*y e. B ph) <-> (E.x e. A E.y e. B ph /\ E.zE.wA.x e. A A.y e. B (ph -> (x = z /\ y = w))))

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

Allowed substitution hints:   ph(x,y)   A(x)   B(y)

Proof of Theorem 2reu5lem3

Step	Hyp	Ref	Expression
1		2reu5lem1 3042	. . 3 |- (E!x e. A E!y e. B ph <-> E!xE!y(x e. A /\ y e. B /\ ph))
2		2reu5lem2 3043	. . 3 |- (A.x e. A E*y e. B ph <-> A.xE*y(x e. A /\ y e. B /\ ph))
3	1, 2	anbi12i 678	. 2 |- ((E!x e. A E!y e. B ph /\ A.x e. A E*y e. B ph) <-> (E!xE!y(x e. A /\ y e. B /\ ph) /\ A.xE*y(x e. A /\ y e. B /\ ph)))
4		2eu5 2288	. 2 |- ((E!xE!y(x e. A /\ y e. B /\ ph) /\ A.xE*y(x e. A /\ y e. B /\ ph)) <-> (E.xE.y(x e. A /\ y e. B /\ ph) /\ E.zE.wA.xA.y((x e. A /\ y e. B /\ ph) -> (x = z /\ y = w))))
5		3anass 938	. . . . . . 7 |- ((x e. A /\ y e. B /\ ph) <-> (x e. A /\ (y e. B /\ ph)))
6	5	exbii 1582	. . . . . 6 |- (E.y(x e. A /\ y e. B /\ ph) <-> E.y(x e. A /\ (y e. B /\ ph)))
7		19.42v 1905	. . . . . 6 |- (E.y(x e. A /\ (y e. B /\ ph)) <-> (x e. A /\ E.y(y e. B /\ ph)))
8		df-rex 2621	. . . . . . . 8 |- (E.y e. B ph <-> E.y(y e. B /\ ph))
9	8	bicomi 193	. . . . . . 7 |- (E.y(y e. B /\ ph) <-> E.y e. B ph)
10	9	anbi2i 675	. . . . . 6 |- ((x e. A /\ E.y(y e. B /\ ph)) <-> (x e. A /\ E.y e. B ph))
11	6, 7, 10	3bitri 262	. . . . 5 |- (E.y(x e. A /\ y e. B /\ ph) <-> (x e. A /\ E.y e. B ph))
12	11	exbii 1582	. . . 4 |- (E.xE.y(x e. A /\ y e. B /\ ph) <-> E.x(x e. A /\ E.y e. B ph))
13		df-rex 2621	. . . 4 |- (E.x e. A E.y e. B ph <-> E.x(x e. A /\ E.y e. B ph))
14	12, 13	bitr4i 243	. . 3 |- (E.xE.y(x e. A /\ y e. B /\ ph) <-> E.x e. A E.y e. B ph)
15		3anan12 947	. . . . . . . . . . 11 |- ((x e. A /\ y e. B /\ ph) <-> (y e. B /\ (x e. A /\ ph)))
16	15	imbi1i 315	. . . . . . . . . 10 |- (((x e. A /\ y e. B /\ ph) -> (x = z /\ y = w)) <-> ((y e. B /\ (x e. A /\ ph)) -> (x = z /\ y = w)))
17		impexp 433	. . . . . . . . . 10 |- (((y e. B /\ (x e. A /\ ph)) -> (x = z /\ y = w)) <-> (y e. B -> ((x e. A /\ ph) -> (x = z /\ y = w))))
18		impexp 433	. . . . . . . . . . 11 |- (((x e. A /\ ph) -> (x = z /\ y = w)) <-> (x e. A -> (ph -> (x = z /\ y = w))))
19	18	imbi2i 303	. . . . . . . . . 10 |- ((y e. B -> ((x e. A /\ ph) -> (x = z /\ y = w))) <-> (y e. B -> (x e. A -> (ph -> (x = z /\ y = w)))))
20	16, 17, 19	3bitri 262	. . . . . . . . 9 |- (((x e. A /\ y e. B /\ ph) -> (x = z /\ y = w)) <-> (y e. B -> (x e. A -> (ph -> (x = z /\ y = w)))))
21	20	albii 1566	. . . . . . . 8 |- (A.y((x e. A /\ y e. B /\ ph) -> (x = z /\ y = w)) <-> A.y(y e. B -> (x e. A -> (ph -> (x = z /\ y = w)))))
22		df-ral 2620	. . . . . . . 8 |- (A.y e. B (x e. A -> (ph -> (x = z /\ y = w))) <-> A.y(y e. B -> (x e. A -> (ph -> (x = z /\ y = w)))))
23		r19.21v 2702	. . . . . . . 8 |- (A.y e. B (x e. A -> (ph -> (x = z /\ y = w))) <-> (x e. A -> A.y e. B (ph -> (x = z /\ y = w))))
24	21, 22, 23	3bitr2i 264	. . . . . . 7 |- (A.y((x e. A /\ y e. B /\ ph) -> (x = z /\ y = w)) <-> (x e. A -> A.y e. B (ph -> (x = z /\ y = w))))
25	24	albii 1566	. . . . . 6 |- (A.xA.y((x e. A /\ y e. B /\ ph) -> (x = z /\ y = w)) <-> A.x(x e. A -> A.y e. B (ph -> (x = z /\ y = w))))
26		df-ral 2620	. . . . . 6 |- (A.x e. A A.y e. B (ph -> (x = z /\ y = w)) <-> A.x(x e. A -> A.y e. B (ph -> (x = z /\ y = w))))
27	25, 26	bitr4i 243	. . . . 5 |- (A.xA.y((x e. A /\ y e. B /\ ph) -> (x = z /\ y = w)) <-> A.x e. A A.y e. B (ph -> (x = z /\ y = w)))
28	27	exbii 1582	. . . 4 |- (E.wA.xA.y((x e. A /\ y e. B /\ ph) -> (x = z /\ y = w)) <-> E.wA.x e. A A.y e. B (ph -> (x = z /\ y = w)))
29	28	exbii 1582	. . 3 |- (E.zE.wA.xA.y((x e. A /\ y e. B /\ ph) -> (x = z /\ y = w)) <-> E.zE.wA.x e. A A.y e. B (ph -> (x = z /\ y = w)))
30	14, 29	anbi12i 678	. 2 |- ((E.xE.y(x e. A /\ y e. B /\ ph) /\ E.zE.wA.xA.y((x e. A /\ y e. B /\ ph) -> (x = z /\ y = w))) <-> (E.x e. A E.y e. B ph /\ E.zE.wA.x e. A A.y e. B (ph -> (x = z /\ y = w))))
31	3, 4, 30	3bitri 262	1 |- ((E!x e. A E!y e. B ph /\ A.x e. A E*y e. B ph) <-> (E.x e. A E.y e. B ph /\ E.zE.wA.x e. A A.y e. B (ph -> (x = z /\ y = w))))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358   /\ w3a 934  A.wal 1540  E.wex 1541   e. wcel 1710  E!weu 2204  E*wmo 2205  A.wral 2615  E.wrex 2616  E!wreu 2617  E*wrmo 2618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623

This theorem is referenced by:  2reu5  3045