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 
 |-  -. (/) e. ( _V X. _V )
2 dmsnn0 
 |-  ( (/) e. ( _V X. _V ) <-> dom { (/) } =/= (/) )
3 2 necon2bbii 
 |-  ( dom { (/) } = (/) <-> -. (/) e. ( _V X. _V ) )
4 1 3 mpbir 
 |-  dom { (/) } = (/)