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 ) )