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

Metamath Proof Explorer

Theorem 2reu2

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

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

Proof

Step Hyp Ref Expression
1 reurmo 
 |-  ( E! y e. B E. x e. A ph -> E* y e. B E. x e. A ph )
2 2rmorex 
 |-  ( E* y e. B E. x e. A ph -> A. x e. A E* y e. B ph )
3 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 ) ) )
4 simpl 
 |-  ( ( 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 )
5 3 4 biimtrdi 
 |-  ( 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 ) )
6 1 2 5 3syl 
 |-  ( 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 ) )
7 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 )
8 7 expcom 
 |-  ( 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 ) )
9 6 8 impbid 
 |-  ( 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 ) )