Metamath Proof Explorer

Theorem 2reu3

Description: Double restricted existential uniqueness, analogous to 2eu3 . (Contributed by Alexander van der Vekens, 29-Jun-2017)

Ref Expression
Assertion 2reu3 
|- ( A. x e. A A. y e. B ( E* x e. A ph \/ 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 ) ) )

Proof

Step Hyp Ref Expression
1 orcom 
 |-  ( ( E* x e. A ph \/ E* y e. B ph ) <-> ( E* y e. B ph \/ E* x e. A ph ) )
2 1 ralbii 
 |-  ( A. y e. B ( E* x e. A ph \/ E* y e. B ph ) <-> A. y e. B ( E* y e. B ph \/ E* x e. A ph ) )
3 nfrmo1 
 |-  F/ y E* y e. B ph
4 3 r19.32 
 |-  ( A. y e. B ( E* y e. B ph \/ E* x e. A ph ) <-> ( E* y e. B ph \/ A. y e. B E* x e. A ph ) )
5 2 4 bitri 
 |-  ( A. y e. B ( E* x e. A ph \/ E* y e. B ph ) <-> ( E* y e. B ph \/ A. y e. B E* x e. A ph ) )
6 orcom 
 |-  ( ( E* y e. B ph \/ A. y e. B E* x e. A ph ) <-> ( A. y e. B E* x e. A ph \/ E* y e. B ph ) )
7 5 6 bitri 
 |-  ( A. y e. B ( E* x e. A ph \/ E* y e. B ph ) <-> ( A. y e. B E* x e. A ph \/ E* y e. B ph ) )
8 7 ralbii 
 |-  ( A. x e. A A. y e. B ( E* x e. A ph \/ E* y e. B ph ) <-> A. x e. A ( A. y e. B E* x e. A ph \/ E* y e. B ph ) )
9 nfcv 
 |-  F/_ x B
10 nfrmo1 
 |-  F/ x E* x e. A ph
11 9 10 nfralw 
 |-  F/ x A. y e. B E* x e. A ph
12 11 r19.32 
 |-  ( A. x e. A ( A. y e. B E* x e. A ph \/ E* y e. B ph ) <-> ( A. y e. B E* x e. A ph \/ A. x e. A E* y e. B ph ) )
13 8 12 bitri 
 |-  ( A. x e. A A. y e. B ( E* x e. A ph \/ E* y e. B ph ) <-> ( A. y e. B E* x e. A ph \/ A. x e. A E* y e. B ph ) )
14 2reu1 
 |-  ( A. 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 /\ E! x e. A E. y e. B ph ) ) )
15 14 biimpd 
 |-  ( A. 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 /\ E! x e. A E. y e. B ph ) ) )
16 ancom 
 |-  ( ( 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 ) )
17 15 16 syl6ib 
 |-  ( A. 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 ) ) )
18 17 adantld 
 |-  ( A. 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 ) ) )
19 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 ) ) )
20 19 biimpd 
 |-  ( 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 ) ) )
21 20 adantrd 
 |-  ( 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 ) ) )
22 18 21 jaoi 
 |-  ( ( A. y e. B E* x e. A 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 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 )
24 2rexreu 
 |-  ( ( 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 )
25 24 ancoms 
 |-  ( ( 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 23 25 jca 
 |-  ( ( 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 22 26 impbid1 
 |-  ( ( A. y e. B E* x e. A 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 ) ) )
28 13 27 sylbi 
 |-  ( A. x e. A A. y e. B ( E* x e. A ph \/ 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 ) ) )