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

Metamath Proof Explorer

Theorem dmsn0

Description: The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004)

Ref Expression
Assertion dmsn0 ⊢ dom ⁡ ∅ = ∅

Proof

Step Hyp Ref Expression
1 0nelxp ⊢ ¬ ∅ ∈ V × V
2 dmsnn0 ⊢ ∅ ∈ V × V ↔ dom ⁡ ∅ ≠ ∅
3 2 necon2bbii ⊢ dom ⁡ ∅ = ∅ ↔ ¬ ∅ ∈ V × V
4 1 3 mpbir ⊢ dom ⁡ ∅ = ∅