This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2reu5

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

Ref Expression
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 r19.29r 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( ( ph /\ ( ph -> ( x = z /\ y = w ) ) ) -> ( x = z /\ y = w ) )
5 4 reximi 
 |-  ( E. y e. B ( ph /\ ( ph -> ( x = z /\ y = w ) ) ) -> E. y e. B ( x = z /\ y = w ) )
6 5 reximi 
 |-  ( 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 eleq1w 
 |-  ( x = z -> ( x e. A <-> z e. A ) )
8 eleq1w 
 |-  ( y = w -> ( y e. B <-> w e. B ) )
9 7 8 bi2anan9 
 |-  ( ( x = z /\ y = w ) -> ( ( x e. A /\ y e. B ) <-> ( z e. A /\ w e. B ) ) )
10 9 biimpac 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( x = z /\ y = w ) ) -> ( z e. A /\ w e. B ) )
11 10 ancomd 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( x = z /\ y = w ) ) -> ( w e. B /\ z e. A ) )
12 11 ex 
 |-  ( ( x e. A /\ y e. B ) -> ( ( x = z /\ y = w ) -> ( w e. B /\ z e. A ) ) )
13 12 rexlimivv 
 |-  ( E. x e. A E. y e. B ( x = z /\ y = w ) -> ( w e. B /\ z e. A ) )
14 1 3 6 13 4syl 
 |-  ( ( 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 ) )
15 14 ex 
 |-  ( 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 pm4.71rd 
 |-  ( 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 ) ) ) ) )
17 anass 
 |-  ( ( ( 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 ) ) ) ) )
18 16 17 bitrdi 
 |-  ( 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 ) ) ) ) ) )
19 18 2exbidv 
 |-  ( E. x e. A E. y e. B ph -> ( E. z E. w A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> E. z E. w ( w e. B /\ ( z e. A /\ A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) ) )
20 19 pm5.32i 
 |-  ( ( E. x e. A E. y e. B ph /\ E. z E. w A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) <-> ( E. x e. A E. y e. B ph /\ E. z E. w ( w e. B /\ ( z e. A /\ A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) ) )
21 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. z E. w A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) )
22 df-rex 
 |-  ( 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 ) ) ) )
23 r19.42v 
 |-  ( 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 ) ) ) )
24 df-rex 
 |-  ( 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 ) ) ) ) )
25 23 24 bitr3i 
 |-  ( ( 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 ) ) ) ) )
26 25 exbii 
 |-  ( E. z ( z e. A /\ E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) <-> E. z E. w ( w e. B /\ ( z e. A /\ A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) )
27 22 26 bitri 
 |-  ( E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) <-> E. z E. w ( w e. B /\ ( z e. A /\ A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) )
28 27 anbi2i 
 |-  ( ( 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. z E. w ( w e. B /\ ( z e. A /\ A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) ) )
29 20 21 28 3bitr4i 
 |-  ( ( 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 ) ) ) )