Metamath Proof Explorer

Theorem 2reu5lem3

Description: Lemma for 2reu5 . 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 . (Contributed by Alexander van der Vekens, 17-Jun-2017)

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

Proof

Step Hyp Ref Expression
1 2reu5lem1 
 |-  ( E! x e. A E! y e. B ph <-> E! x E! y ( x e. A /\ y e. B /\ ph ) )
2 2reu5lem2 
 |-  ( A. x e. A E* y e. B ph <-> A. x E* y ( x e. A /\ y e. B /\ ph ) )
3 1 2 anbi12i 
 |-  ( ( E! x e. A E! y e. B ph /\ A. x e. A E* y e. B ph ) <-> ( E! x E! y ( x e. A /\ y e. B /\ ph ) /\ A. x E* y ( x e. A /\ y e. B /\ ph ) ) )
4 2eu5 
 |-  ( ( E! x E! y ( x e. A /\ y e. B /\ ph ) /\ A. x E* y ( x e. A /\ y e. B /\ ph ) ) <-> ( E. x E. y ( x e. A /\ y e. B /\ ph ) /\ E. z E. w A. x A. y ( ( x e. A /\ y e. B /\ ph ) -> ( x = z /\ y = w ) ) ) )
5 3anass 
 |-  ( ( x e. A /\ y e. B /\ ph ) <-> ( x e. A /\ ( y e. B /\ ph ) ) )
6 5 exbii 
 |-  ( E. y ( x e. A /\ y e. B /\ ph ) <-> E. y ( x e. A /\ ( y e. B /\ ph ) ) )
7 19.42v 
 |-  ( E. y ( x e. A /\ ( y e. B /\ ph ) ) <-> ( x e. A /\ E. y ( y e. B /\ ph ) ) )
8 df-rex 
 |-  ( E. y e. B ph <-> E. y ( y e. B /\ ph ) )
9 8 bicomi 
 |-  ( E. y ( y e. B /\ ph ) <-> E. y e. B ph )
10 9 anbi2i 
 |-  ( ( x e. A /\ E. y ( y e. B /\ ph ) ) <-> ( x e. A /\ E. y e. B ph ) )
11 6 7 10 3bitri 
 |-  ( E. y ( x e. A /\ y e. B /\ ph ) <-> ( x e. A /\ E. y e. B ph ) )
12 11 exbii 
 |-  ( E. x E. y ( x e. A /\ y e. B /\ ph ) <-> E. x ( x e. A /\ E. y e. B ph ) )
13 df-rex 
 |-  ( E. x e. A E. y e. B ph <-> E. x ( x e. A /\ E. y e. B ph ) )
14 12 13 bitr4i 
 |-  ( E. x E. y ( x e. A /\ y e. B /\ ph ) <-> E. x e. A E. y e. B ph )
15 3anan12 
 |-  ( ( x e. A /\ y e. B /\ ph ) <-> ( y e. B /\ ( x e. A /\ ph ) ) )
16 15 imbi1i 
 |-  ( ( ( x e. A /\ y e. B /\ ph ) -> ( x = z /\ y = w ) ) <-> ( ( y e. B /\ ( x e. A /\ ph ) ) -> ( x = z /\ y = w ) ) )
17 impexp 
 |-  ( ( ( y e. B /\ ( x e. A /\ ph ) ) -> ( x = z /\ y = w ) ) <-> ( y e. B -> ( ( x e. A /\ ph ) -> ( x = z /\ y = w ) ) ) )
18 impexp 
 |-  ( ( ( x e. A /\ ph ) -> ( x = z /\ y = w ) ) <-> ( x e. A -> ( ph -> ( x = z /\ y = w ) ) ) )
19 18 imbi2i 
 |-  ( ( 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 
 |-  ( ( ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( A. x A. 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 
 |-  ( 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 
 |-  ( A. x A. 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 
 |-  ( E. w A. x A. y ( ( x e. A /\ y e. B /\ ph ) -> ( x = z /\ y = w ) ) <-> E. w A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) )
29 28 exbii 
 |-  ( E. z E. w A. x A. y ( ( x e. A /\ y e. B /\ ph ) -> ( x = z /\ y = w ) ) <-> E. z E. w A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) )
30 14 29 anbi12i 
 |-  ( ( E. x E. y ( x e. A /\ y e. B /\ ph ) /\ E. z E. w A. x A. y ( ( x e. A /\ y e. B /\ ph ) -> ( x = z /\ y = w ) ) ) <-> ( 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 ) ) ) )
31 3 4 30 3bitri 
 |-  ( ( 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 ) ) ) )