Metamath Proof Explorer

Theorem rsp2e

Description: Restricted specialization. (Contributed by FL, 4-Jun-2012) (Proof shortened by Wolf Lammen, 7-Jan-2020)

Ref Expression
Assertion rsp2e 
|- ( ( x e. A /\ y e. B /\ ph ) -> E. x e. A E. y e. B ph )

Proof

Step Hyp Ref Expression
1 rspe 
 |-  ( ( y e. B /\ ph ) -> E. y e. B ph )
2 rspe 
 |-  ( ( x e. A /\ E. y e. B ph ) -> E. x e. A E. y e. B ph )
3 1 2 sylan2 
 |-  ( ( x e. A /\ ( y e. B /\ ph ) ) -> E. x e. A E. y e. B ph )
4 3 3impb 
 |-  ( ( x e. A /\ y e. B /\ ph ) -> E. x e. A E. y e. B ph )