Metamath Proof Explorer

Theorem ssrab2

Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997) (Proof shortened by BJ and SN, 8-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 elrabi ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } → 𝑦 ∈ 𝐴 )
2 1 ssriv ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴