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	ralrimiva	|- ( ph -> A. x e. A ( ps -> ch ) )
3	2	ss2rabd	|- ( ph -> { x e. A | ps } C_ { x e. A | ch } )