Theorem ssrab3

Description: Subclass relation for a restricted class abstraction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

	Ref	Expression
Hypothesis	ssrab3.1	⊢ 𝐵 = { 𝑥 ∈ 𝐴 ∣ 𝜑 }
Assertion	ssrab3	⊢ 𝐵 ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		ssrab3.1	⊢ 𝐵 = { 𝑥 ∈ 𝐴 ∣ 𝜑 }
2		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴
3	1 2	eqsstri	⊢ 𝐵 ⊆ 𝐴