Theorem ssrab3

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

	Ref	Expression
Hypothesis	ssrab3.1	$$⊢B=\left\{x\in A|\phi \right\}$$
Assertion	ssrab3	$$⊢B\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		ssrab3.1	$$⊢B=\left\{x\in A|\phi \right\}$$
2		ssrab2	$$⊢\left\{x\in A|\phi \right\}\subseteq A$$
3	1 2	eqsstri	$$⊢B\subseteq A$$