This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ 𝐴