Metamath Proof Explorer

Theorem ssralv

Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006)

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

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( A C_ B -> ( x e. A -> x e. B ) )
2 1 imim1d 
 |-  ( A C_ B -> ( ( x e. B -> ph ) -> ( x e. A -> ph ) ) )
3 2 ralimdv2 
 |-  ( A C_ B -> ( A. x e. B ph -> A. x e. A ph ) )