Metamath Proof Explorer

Theorem rnsnn0

Description: The range of a singleton is nonzero iff the singleton argument is an ordered pair. (Contributed by NM, 14-Dec-2008)

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

Proof

Step Hyp Ref Expression
1 dmsnn0 
 |-  ( A e. ( _V X. _V ) <-> dom { A } =/= (/) )
2 dm0rn0 
 |-  ( dom { A } = (/) <-> ran { A } = (/) )
3 2 necon3bii 
 |-  ( dom { A } =/= (/) <-> ran { A } =/= (/) )
4 1 3 bitri 
 |-  ( A e. ( _V X. _V ) <-> ran { A } =/= (/) )