Theorem ssrab3

Description: Subclass relation for a restricted class abstraction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

	Ref	Expression
Hypothesis	ssrab3.1	|- B = { x e. A | ph }
Assertion	ssrab3	|- B C_ A

Proof

Step	Hyp	Ref	Expression
1		ssrab3.1	|- B = { x e. A | ph }
2		ssrab2	|- { x e. A | ph } C_ A
3	1 2	eqsstri	|- B C_ A