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

Metamath Proof Explorer

Theorem dmsn0el

Description: The domain of a singleton is empty if the singleton's argument contains the empty set. (Contributed by NM, 15-Dec-2008)

Ref Expression
Assertion dmsn0el ⊢ ∅ ∈ A → dom ⁡ A = ∅

Proof

Step Hyp Ref Expression
1 dmsnn0 ⊢ A ∈ V × V ↔ dom ⁡ A ≠ ∅
2 0nelelxp ⊢ A ∈ V × V → ¬ ∅ ∈ A
3 1 2 sylbir ⊢ dom ⁡ A ≠ ∅ → ¬ ∅ ∈ A
4 3 necon4ai ⊢ ∅ ∈ A → dom ⁡ A = ∅