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 
|- ( (/) e. A -> dom { A } = (/) )

Proof

Step Hyp Ref Expression
1 dmsnn0 
 |-  ( A e. ( _V X. _V ) <-> dom { A } =/= (/) )
2 0nelelxp 
 |-  ( A e. ( _V X. _V ) -> -. (/) e. A )
3 1 2 sylbir 
 |-  ( dom { A } =/= (/) -> -. (/) e. A )
4 3 necon4ai 
 |-  ( (/) e. A -> dom { A } = (/) )