Theorem rabss2

Description: Subclass law for restricted abstraction. (Contributed by NM, 18-Dec-2004) (Proof shortened by Andrew Salmon, 26-Jun-2011) Avoid axioms. (Revised by TM, 1-Feb-2026)

	Ref	Expression
Assertion	rabss2	|- ( A C_ B -> { x e. A | ph } C_ { x e. B | ph } )

Proof

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