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