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

Metamath Proof Explorer

Theorem dmsnn0

Description: The domain of a singleton is nonzero iff the singleton argument is an ordered pair. (Contributed by NM, 14-Dec-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion dmsnn0 
|- ( A e. ( _V X. _V ) <-> dom { A } =/= (/) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 eldm 
 |-  ( x e. dom { A } <-> E. y x { A } y )
3 df-br 
 |-  ( x { A } y <-> <. x , y >. e. { A } )
4 opex 
 |-  <. x , y >. e. _V
5 4 elsn 
 |-  ( <. x , y >. e. { A } <-> <. x , y >. = A )
6 eqcom 
 |-  ( <. x , y >. = A <-> A = <. x , y >. )
7 3 5 6 3bitri 
 |-  ( x { A } y <-> A = <. x , y >. )
8 7 exbii 
 |-  ( E. y x { A } y <-> E. y A = <. x , y >. )
9 2 8 bitr2i 
 |-  ( E. y A = <. x , y >. <-> x e. dom { A } )
10 9 exbii 
 |-  ( E. x E. y A = <. x , y >. <-> E. x x e. dom { A } )
11 elvv 
 |-  ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )
12 n0 
 |-  ( dom { A } =/= (/) <-> E. x x e. dom { A } )
13 10 11 12 3bitr4i 
 |-  ( A e. ( _V X. _V ) <-> dom { A } =/= (/) )