Theorem 2reu5 3045

Description: Double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, analogous to 2eu5 2288 and reu3 3027. (Contributed by Alexander van der Vekens, 17-Jun-2017.)

Assertion

Ref	Expression
2reu5	|- ((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.z e. A E.w e. B A.x e. A A.y e. B (ph -> (x = z /\ y = w))))

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

Allowed substitution hints:   ph(x,y)

Proof of Theorem 2reu5

Step	Hyp	Ref	Expression
1		r19.29r 2756	. . . . . . . 8 |- ((E.x e. A E.y e. B ph /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w))) -> E.x e. A (E.y e. B ph /\ A.y e. B (ph -> (x = z /\ y = w))))
2		r19.29r 2756	. . . . . . . . 9 |- ((E.y e. B ph /\ A.y e. B (ph -> (x = z /\ y = w))) -> E.y e. B (ph /\ (ph -> (x = z /\ y = w))))
3	2	reximi 2722	. . . . . . . 8 |- (E.x e. A (E.y e. B ph /\ A.y e. B (ph -> (x = z /\ y = w))) -> E.x e. A E.y e. B (ph /\ (ph -> (x = z /\ y = w))))
4		pm3.35 570	. . . . . . . . . . 11 |- ((ph /\ (ph -> (x = z /\ y = w))) -> (x = z /\ y = w))
5	4	reximi 2722	. . . . . . . . . 10 |- (E.y e. B (ph /\ (ph -> (x = z /\ y = w))) -> E.y e. B (x = z /\ y = w))
6	5	reximi 2722	. . . . . . . . 9 |- (E.x e. A E.y e. B (ph /\ (ph -> (x = z /\ y = w))) -> E.x e. A E.y e. B (x = z /\ y = w))
7		eleq1 2413	. . . . . . . . . . . . . 14 |- (x = z -> (x e. A <-> z e. A))
8		eleq1 2413	. . . . . . . . . . . . . 14 |- (y = w -> (y e. B <-> w e. B))
9	7, 8	bi2anan9 843	. . . . . . . . . . . . 13 |- ((x = z /\ y = w) -> ((x e. A /\ y e. B) <-> (z e. A /\ w e. B)))
10	9	biimpac 472	. . . . . . . . . . . 12 |- (((x e. A /\ y e. B) /\ (x = z /\ y = w)) -> (z e. A /\ w e. B))
11	10	ancomd 438	. . . . . . . . . . 11 |- (((x e. A /\ y e. B) /\ (x = z /\ y = w)) -> (w e. B /\ z e. A))
12	11	ex 423	. . . . . . . . . 10 |- ((x e. A /\ y e. B) -> ((x = z /\ y = w) -> (w e. B /\ z e. A)))
13	12	rexlimivv 2744	. . . . . . . . 9 |- (E.x e. A E.y e. B (x = z /\ y = w) -> (w e. B /\ z e. A))
14	6, 13	syl 15	. . . . . . . 8 |- (E.x e. A E.y e. B (ph /\ (ph -> (x = z /\ y = w))) -> (w e. B /\ z e. A))
15	1, 3, 14	3syl 18	. . . . . . 7 |- ((E.x e. A E.y e. B ph /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w))) -> (w e. B /\ z e. A))
16	15	ex 423	. . . . . 6 |- (E.x e. A E.y e. B ph -> (A.x e. A A.y e. B (ph -> (x = z /\ y = w)) -> (w e. B /\ z e. A)))
17	16	pm4.71rd 616	. . . . 5 |- (E.x e. A E.y e. B ph -> (A.x e. A A.y e. B (ph -> (x = z /\ y = w)) <-> ((w e. B /\ z e. A) /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w)))))
18		anass 630	. . . . 5 |- (((w e. B /\ z e. A) /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w))) <-> (w e. B /\ (z e. A /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w)))))
19	17, 18	syl6bb 252	. . . 4 |- (E.x e. A E.y e. B ph -> (A.x e. A A.y e. B (ph -> (x = z /\ y = w)) <-> (w e. B /\ (z e. A /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w))))))
20	19	2exbidv 1628	. . 3 |- (E.x e. A E.y e. B ph -> (E.zE.wA.x e. A A.y e. B (ph -> (x = z /\ y = w)) <-> E.zE.w(w e. B /\ (z e. A /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w))))))
21	20	pm5.32i 618	. 2 |- ((E.x e. A E.y e. B ph /\ E.zE.wA.x e. A A.y e. B (ph -> (x = z /\ y = w))) <-> (E.x e. A E.y e. B ph /\ E.zE.w(w e. B /\ (z e. A /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w))))))
22		2reu5lem3 3044	. 2 |- ((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))))
23		df-rex 2621	. . . 4 |- (E.z e. A E.w e. B A.x e. A A.y e. B (ph -> (x = z /\ y = w)) <-> E.z(z e. A /\ E.w e. B A.x e. A A.y e. B (ph -> (x = z /\ y = w))))
24		r19.42v 2766	. . . . . 6 |- (E.w e. B (z e. A /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w))) <-> (z e. A /\ E.w e. B A.x e. A A.y e. B (ph -> (x = z /\ y = w))))
25		df-rex 2621	. . . . . 6 |- (E.w e. B (z e. A /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w))) <-> E.w(w e. B /\ (z e. A /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w)))))
26	24, 25	bitr3i 242	. . . . 5 |- ((z e. A /\ E.w e. B A.x e. A A.y e. B (ph -> (x = z /\ y = w))) <-> E.w(w e. B /\ (z e. A /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w)))))
27	26	exbii 1582	. . . 4 |- (E.z(z e. A /\ E.w e. B A.x e. A A.y e. B (ph -> (x = z /\ y = w))) <-> E.zE.w(w e. B /\ (z e. A /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w)))))
28	23, 27	bitri 240	. . 3 |- (E.z e. A E.w e. B A.x e. A A.y e. B (ph -> (x = z /\ y = w)) <-> E.zE.w(w e. B /\ (z e. A /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w)))))
29	28	anbi2i 675	. 2 |- ((E.x e. A E.y e. B ph /\ E.z e. A E.w e. B A.x e. A A.y e. B (ph -> (x = z /\ y = w))) <-> (E.x e. A E.y e. B ph /\ E.zE.w(w e. B /\ (z e. A /\ A.x e. A A.y e. B (ph -> (x = z /\ y = w))))))
30	21, 22, 29	3bitr4i 268	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.z e. A E.w e. B A.x e. A A.y e. B (ph -> (x = z /\ y = w))))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358  E.wex 1541   e. wcel 1710  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  ax-ext 2334

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-cleq 2346  df-clel 2349  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623

This theorem is referenced by: (None)