Theorem rabssab

Description: A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016)

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

Proof

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