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

Metamath Proof Explorer

Theorem ssrab2f

Description: Subclass relation for a restricted class. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis ssrab2f.1 ⊢ Ⅎ 𝑥 𝐴
Assertion ssrab2f { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴

Proof

Step Hyp Ref Expression
1 ssrab2f.1 ⊢ Ⅎ 𝑥 𝐴
2 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝜑 }
3 2 1 dfss3f ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 ↔ ∀ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } 𝑥 ∈ 𝐴 )
4 rabidim1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } → 𝑥 ∈ 𝐴 )
5 3 4 mprgbir ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴