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

Metamath Proof Explorer

Theorem abssdv

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006) (Proof shortened by SN, 22-Dec-2024)

Ref Expression
Hypothesis abssdv.1 ⊢ ( 𝜑 → ( 𝜓 → 𝑥 ∈ 𝐴 ) )
Assertion abssdv ( 𝜑 → { 𝑥 ∣ 𝜓 } ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 abssdv.1 ⊢ ( 𝜑 → ( 𝜓 → 𝑥 ∈ 𝐴 ) )
2 1 ss2abdv ⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } ⊆ { 𝑥 ∣ 𝑥 ∈ 𝐴 } )
3 abid1 ⊢ 𝐴 = { 𝑥 ∣ 𝑥 ∈ 𝐴 }
4 2 3 sseqtrrdi ⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } ⊆ 𝐴 )