Metamath Proof Explorer

Theorem 2reu2rex

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

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

Proof

Step Hyp Ref Expression
1 reurex 
 |-  ( 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 reximi 
 |-  ( 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 )