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

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