Theorem ssab2

Description: Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995)

	Ref	Expression
Assertion	ssab2	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(x\in A\wedge \phi \right)\to x\in A$$
2	1	abssi	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}\subseteq A$$