Metamath Proof Explorer


Theorem ss2ab1

Description: Class abstractions in a subclass relationship, closed form. One direction of ss2ab using fewer axioms. (Contributed by SN, 22-Dec-2024)

Ref Expression
Assertion ss2ab1 ( ∀ 𝑥 ( 𝜑𝜓 ) → { 𝑥𝜑 } ⊆ { 𝑥𝜓 } )

Proof

Step Hyp Ref Expression
1 spsbim ( ∀ 𝑥 ( 𝜑𝜓 ) → ( [ 𝑡 / 𝑥 ] 𝜑 → [ 𝑡 / 𝑥 ] 𝜓 ) )
2 df-clab ( 𝑡 ∈ { 𝑥𝜑 } ↔ [ 𝑡 / 𝑥 ] 𝜑 )
3 df-clab ( 𝑡 ∈ { 𝑥𝜓 } ↔ [ 𝑡 / 𝑥 ] 𝜓 )
4 1 2 3 3imtr4g ( ∀ 𝑥 ( 𝜑𝜓 ) → ( 𝑡 ∈ { 𝑥𝜑 } → 𝑡 ∈ { 𝑥𝜓 } ) )
5 4 ssrdv ( ∀ 𝑥 ( 𝜑𝜓 ) → { 𝑥𝜑 } ⊆ { 𝑥𝜓 } )