Theorem ssrab2

Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997)

	Ref	Expression
Assertion	ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴

Proof

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