Metamath Proof Explorer

Theorem ssab2

Description: Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995)

Ref Expression
Assertion ssab2 { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → 𝑥 ∈ 𝐴 )
2 1 abssi ⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴