Metamath Proof Explorer

Theorem ssrexv

Description: Existential quantification restricted to a subclass. (Contributed by NM, 11-Jan-2007)

Ref Expression
Assertion ssrexv 
|- ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( A C_ B -> ( x e. A -> x e. B ) )
2 1 anim1d 
 |-  ( A C_ B -> ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) )
3 2 reximdv2 
 |-  ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )