Metamath Proof Explorer


Theorem eq0rdv

Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014)

Ref Expression
Hypothesis eq0rdv.1 ( 𝜑 → ¬ 𝑥𝐴 )
Assertion eq0rdv ( 𝜑𝐴 = ∅ )

Proof

Step Hyp Ref Expression
1 eq0rdv.1 ( 𝜑 → ¬ 𝑥𝐴 )
2 1 pm2.21d ( 𝜑 → ( 𝑥𝐴𝑥 ∈ ∅ ) )
3 2 ssrdv ( 𝜑𝐴 ⊆ ∅ )
4 ss0 ( 𝐴 ⊆ ∅ → 𝐴 = ∅ )
5 3 4 syl ( 𝜑𝐴 = ∅ )