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 } =/= (/) )