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

Metamath Proof Explorer

Theorem ss2rabd

Description: Subclass of a restricted class abstraction (deduction form). Saves ax-10 , ax-11 , ax-12 over using ss2rab and sylibr . (Contributed by SN, 4-Feb-2026)

Ref Expression
Hypothesis ss2rabd.1 
|- ( ph -> A. x e. A ( ps -> ch ) )
Assertion ss2rabd 
|- ( ph -> { x e. A | ps } C_ { x e. A | ch } )

Proof

Step Hyp Ref Expression
1 ss2rabd.1 
 |-  ( ph -> A. x e. A ( ps -> ch ) )
2 df-ral 
 |-  ( A. x e. A ( ps -> ch ) <-> A. x ( x e. A -> ( ps -> ch ) ) )
3 imdistan 
 |-  ( ( x e. A -> ( ps -> ch ) ) <-> ( ( x e. A /\ ps ) -> ( x e. A /\ ch ) ) )
4 3 albii 
 |-  ( A. x ( x e. A -> ( ps -> ch ) ) <-> A. x ( ( x e. A /\ ps ) -> ( x e. A /\ ch ) ) )
5 2 4 bitri 
 |-  ( A. x e. A ( ps -> ch ) <-> A. x ( ( x e. A /\ ps ) -> ( x e. A /\ ch ) ) )
6 1 5 sylib 
 |-  ( ph -> A. x ( ( x e. A /\ ps ) -> ( x e. A /\ ch ) ) )
7 ss2abim 
 |-  ( A. x ( ( x e. A /\ ps ) -> ( x e. A /\ ch ) ) -> { x | ( x e. A /\ ps ) } C_ { x | ( x e. A /\ ch ) } )
8 6 7 syl 
 |-  ( ph -> { x | ( x e. A /\ ps ) } C_ { x | ( x e. A /\ ch ) } )
9 df-rab 
 |-  { x e. A | ps } = { x | ( x e. A /\ ps ) }
10 df-rab 
 |-  { x e. A | ch } = { x | ( x e. A /\ ch ) }
11 8 9 10 3sstr4g 
 |-  ( ph -> { x e. A | ps } C_ { x e. A | ch } )