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 { ∅ } = ∅