Theorem ssrab2OLD

Description: Obsolete version of ssrab2 as of 8-Aug-2024. (Contributed by NM, 19-Mar-1997) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	ssrab2OLD	$$⊢\left\{x\in A|\phi \right\}\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
2		ssab2	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}\subseteq A$$
3	1 2	eqsstri	$$⊢\left\{x\in A|\phi \right\}\subseteq A$$