Metamath Proof Explorer


Theorem ss2abdv

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011) (Revised by Steven Nguyen, 28-Jun-2024)

Ref Expression
Hypothesis ss2abdv.1 ( 𝜑 → ( 𝜓𝜒 ) )
Assertion ss2abdv ( 𝜑 → { 𝑥𝜓 } ⊆ { 𝑥𝜒 } )

Proof

Step Hyp Ref Expression
1 ss2abdv.1 ( 𝜑 → ( 𝜓𝜒 ) )
2 1 sbimdv ( 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] 𝜒 ) )
3 df-clab ( 𝑦 ∈ { 𝑥𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 )
4 df-clab ( 𝑦 ∈ { 𝑥𝜒 } ↔ [ 𝑦 / 𝑥 ] 𝜒 )
5 2 3 4 3imtr4g ( 𝜑 → ( 𝑦 ∈ { 𝑥𝜓 } → 𝑦 ∈ { 𝑥𝜒 } ) )
6 5 ssrdv ( 𝜑 → { 𝑥𝜓 } ⊆ { 𝑥𝜒 } )