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

Metamath Proof Explorer

Theorem 2rexreu

Description: Double restricted existential uniqueness implies double restricted unique existential quantification, analogous to 2exeu . (Contributed by Alexander van der Vekens, 25-Jun-2017)

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

Proof

Step Hyp Ref Expression
1 reurmo 
 |-  ( E! x e. A E. y e. B ph -> E* x e. A E. y e. B ph )
2 reurex 
 |-  ( E! y e. B ph -> E. y e. B ph )
3 2 rmoimi 
 |-  ( E* x e. A E. y e. B ph -> E* x e. A E! y e. B ph )
4 1 3 syl 
 |-  ( E! x e. A E. y e. B ph -> E* x e. A E! y e. B ph )
5 2reurex 
 |-  ( E! y e. B E. x e. A ph -> E. x e. A E! y e. B ph )
6 4 5 anim12ci 
 |-  ( ( 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 ) )
7 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 ) )
8 6 7 sylibr 
 |-  ( ( 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 )