Metamath Proof Explorer

Theorem 2reu1

Description: Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 . (Contributed by Alexander van der Vekens, 25-Jun-2017)

Ref Expression
Assertion 2reu1 
|- ( A. x e. A E* y e. B ph -> ( E! x e. A E! y e. B ph <-> ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) ) )

Proof

Step Hyp Ref Expression
1 2reu5a 
 |-  ( E! x e. A E! y e. B ph <-> ( E. x e. A ( E. y e. B ph /\ E* y e. B ph ) /\ E* x e. A ( E. y e. B ph /\ E* y e. B ph ) ) )
2 simprr 
 |-  ( ( x e. A /\ ( A. x e. A E* y e. B ph /\ E. y e. B ph ) ) -> E. y e. B ph )
3 rsp 
 |-  ( A. x e. A E* y e. B ph -> ( x e. A -> E* y e. B ph ) )
4 3 adantr 
 |-  ( ( A. x e. A E* y e. B ph /\ E. y e. B ph ) -> ( x e. A -> E* y e. B ph ) )
5 4 impcom 
 |-  ( ( x e. A /\ ( A. x e. A E* y e. B ph /\ E. y e. B ph ) ) -> E* y e. B ph )
6 2 5 jca 
 |-  ( ( x e. A /\ ( A. x e. A E* y e. B ph /\ E. y e. B ph ) ) -> ( E. y e. B ph /\ E* y e. B ph ) )
7 6 ex 
 |-  ( x e. A -> ( ( A. x e. A E* y e. B ph /\ E. y e. B ph ) -> ( E. y e. B ph /\ E* y e. B ph ) ) )
8 7 rmoimia 
 |-  ( E* x e. A ( E. y e. B ph /\ E* y e. B ph ) -> E* x e. A ( A. x e. A E* y e. B ph /\ E. y e. B ph ) )
9 nfra1 
 |-  F/ x A. x e. A E* y e. B ph
10 9 rmoanim 
 |-  ( E* x e. A ( A. x e. A E* y e. B ph /\ E. y e. B ph ) <-> ( A. x e. A E* y e. B ph -> E* x e. A E. y e. B ph ) )
11 8 10 sylib 
 |-  ( E* x e. A ( E. y e. B ph /\ E* y e. B ph ) -> ( A. x e. A E* y e. B ph -> E* x e. A E. y e. B ph ) )
12 11 ancrd 
 |-  ( E* x e. A ( E. y e. B ph /\ E* y e. B ph ) -> ( A. x e. A E* y e. B ph -> ( E* x e. A E. y e. B ph /\ A. x e. A E* y e. B ph ) ) )
13 2rmoswap 
 |-  ( A. x e. A E* y e. B ph -> ( E* x e. A E. y e. B ph -> E* y e. B E. x e. A ph ) )
14 13 com12 
 |-  ( E* x e. A E. y e. B ph -> ( A. x e. A E* y e. B ph -> E* y e. B E. x e. A ph ) )
15 14 imdistani 
 |-  ( ( 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* y e. B E. x e. A ph ) )
16 12 15 syl6 
 |-  ( E* x e. A ( E. y e. B ph /\ E* y e. B ph ) -> ( A. x e. A E* y e. B ph -> ( E* x e. A E. y e. B ph /\ E* y e. B E. x e. A ph ) ) )
17 1 16 simplbiim 
 |-  ( 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* y e. B E. x e. A ph ) ) )
18 2reu2rex 
 |-  ( E! x e. A E! y e. B ph -> E. x e. A E. y e. B ph )
19 rexcom 
 |-  ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph )
20 18 19 sylib 
 |-  ( E! x e. A E! y e. B ph -> E. y e. B E. x e. A ph )
21 18 20 jca 
 |-  ( E! x e. A E! y e. B ph -> ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) )
22 17 21 jctild 
 |-  ( 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. y e. B E. x e. A ph ) /\ ( E* x e. A E. y e. B ph /\ E* y e. B E. x e. A ph ) ) ) )
23 reu5 
 |-  ( E! x e. A E. y e. B ph <-> ( E. x e. A E. y e. B ph /\ E* x e. A E. y e. B ph ) )
24 reu5 
 |-  ( E! y e. B E. x e. A ph <-> ( E. y e. B E. x e. A ph /\ E* y e. B E. x e. A ph ) )
25 23 24 anbi12i 
 |-  ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( ( E. x e. A E. y e. B ph /\ E* x e. A E. y e. B ph ) /\ ( E. y e. B E. x e. A ph /\ E* y e. B E. x e. A ph ) ) )
26 an4 
 |-  ( ( ( E. x e. A E. y e. B ph /\ E* x e. A E. y e. B ph ) /\ ( E. y e. B E. x e. A ph /\ E* y e. B E. x e. A ph ) ) <-> ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) /\ ( E* x e. A E. y e. B ph /\ E* y e. B E. x e. A ph ) ) )
27 25 26 bitri 
 |-  ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( ( E. x e. A E. y e. B ph /\ E. y e. B E. x e. A ph ) /\ ( E* x e. A E. y e. B ph /\ E* y e. B E. x e. A ph ) ) )
28 22 27 syl6ibr 
 |-  ( 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! y e. B E. x e. A ph ) ) )
29 28 com12 
 |-  ( A. x e. A E* y e. B ph -> ( E! x e. A E! y e. B ph -> ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) ) )
30 2rexreu 
 |-  ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) -> E! x e. A E! y e. B ph )
31 29 30 impbid1 
 |-  ( A. x e. A E* y e. B ph -> ( E! x e. A E! y e. B ph <-> ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) ) )