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

Metamath Proof Explorer

Theorem ssralv

Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006) Avoid axioms. (Revised by GG, 19-May-2025)

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

Proof

Step Hyp Ref Expression
1 df-ss 
 |-  ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2 imim1 
 |-  ( ( x e. A -> x e. B ) -> ( ( x e. B -> ph ) -> ( x e. A -> ph ) ) )
3 2 al2imi 
 |-  ( A. x ( x e. A -> x e. B ) -> ( A. x ( x e. B -> ph ) -> A. x ( x e. A -> ph ) ) )
4 df-ral 
 |-  ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
5 df-ral 
 |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
6 3 4 5 3imtr4g 
 |-  ( A. x ( x e. A -> x e. B ) -> ( A. x e. B ph -> A. x e. A ph ) )
7 1 6 sylbi 
 |-  ( A C_ B -> ( A. x e. B ph -> A. x e. A ph ) )