Metamath Proof Explorer


Theorem ssabdv

Description: Deduction of abstraction subclass from implication. (Contributed by SN, 22-Dec-2024)

Ref Expression
Hypothesis ssabdv.1 ( 𝜑 → ( 𝑥𝐴𝜓 ) )
Assertion ssabdv ( 𝜑𝐴 ⊆ { 𝑥𝜓 } )

Proof

Step Hyp Ref Expression
1 ssabdv.1 ( 𝜑 → ( 𝑥𝐴𝜓 ) )
2 abid1 𝐴 = { 𝑥𝑥𝐴 }
3 1 ss2abdv ( 𝜑 → { 𝑥𝑥𝐴 } ⊆ { 𝑥𝜓 } )
4 2 3 eqsstrid ( 𝜑𝐴 ⊆ { 𝑥𝜓 } )