Theorem ss2rabdv

Description: Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006) Avoid axioms. (Revised by TM, 1-Feb-2026)

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

Proof

Step	Hyp	Ref	Expression
1		ss2rabdv.1	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
2	1	imdistanda	|- ( ph -> ( ( x e. A /\ ps ) -> ( x e. A /\ ch ) ) )
3	2	ss2abdv	|- ( ph -> { x | ( x e. A /\ ps ) } C_ { x | ( x e. A /\ ch ) } )
4		df-rab	|- { x e. A | ps } = { x | ( x e. A /\ ps ) }
5		df-rab	|- { x e. A | ch } = { x | ( x e. A /\ ch ) }
6	3 4 5	3sstr4g	|- ( ph -> { x e. A | ps } C_ { x e. A | ch } )