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

Metamath Proof Explorer

Theorem 2reurex

Description: Double restricted quantification with existential uniqueness, analogous to 2euex . (Contributed by Alexander van der Vekens, 24-Jun-2017)

Ref Expression
Assertion 2reurex 
|- ( E! x e. A E. y e. B ph -> E. y e. B E! x e. A ph )

Proof

Step Hyp Ref Expression
1 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 ) )
2 rexcom 
 |-  ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph )
3 nfcv 
 |-  F/_ y A
4 nfre1 
 |-  F/ y E. y e. B ph
5 3 4 nfrmow 
 |-  F/ y E* x e. A E. y e. B ph
6 rspe 
 |-  ( ( y e. B /\ ph ) -> E. y e. B ph )
7 6 ex 
 |-  ( y e. B -> ( ph -> E. y e. B ph ) )
8 7 ralrimivw 
 |-  ( y e. B -> A. x e. A ( ph -> E. y e. B ph ) )
9 rmoim 
 |-  ( A. x e. A ( ph -> E. y e. B ph ) -> ( E* x e. A E. y e. B ph -> E* x e. A ph ) )
10 8 9 syl 
 |-  ( y e. B -> ( E* x e. A E. y e. B ph -> E* x e. A ph ) )
11 10 impcom 
 |-  ( ( E* x e. A E. y e. B ph /\ y e. B ) -> E* x e. A ph )
12 rmo5 
 |-  ( E* x e. A ph <-> ( E. x e. A ph -> E! x e. A ph ) )
13 11 12 sylib 
 |-  ( ( E* x e. A E. y e. B ph /\ y e. B ) -> ( E. x e. A ph -> E! x e. A ph ) )
14 13 ex 
 |-  ( E* x e. A E. y e. B ph -> ( y e. B -> ( E. x e. A ph -> E! x e. A ph ) ) )
15 5 14 reximdai 
 |-  ( 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 ) )
16 2 15 biimtrid 
 |-  ( 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 16 impcom 
 |-  ( ( 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 )
18 1 17 sylbi 
 |-  ( E! x e. A E. y e. B ph -> E. y e. B E! x e. A ph )