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	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
2		ssab2	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴
3	1 2	eqsstri	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴