Theorem rabssab

Description: A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Assertion	rabssab	|- { x e. A | ph } C_ { x | ph }

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
2		simpr	|- ( ( x e. A /\ ph ) -> ph )
3	2	ss2abi	|- { x | ( x e. A /\ ph ) } C_ { x | ph }
4	1 3	eqsstri	|- { x e. A | ph } C_ { x | ph }