Metamath Proof Explorer

Theorem 0sdomg

Description: A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 23-Mar-2006)

Ref Expression
Assertion 0sdomg 
|- ( A e. V -> ( (/) ~< A <-> A =/= (/) ) )

Proof

Step Hyp Ref Expression
1 0domg 
 |-  ( A e. V -> (/) ~<_ A )
2 brsdom 
 |-  ( (/) ~< A <-> ( (/) ~<_ A /\ -. (/) ~~ A ) )
3 2 baib 
 |-  ( (/) ~<_ A -> ( (/) ~< A <-> -. (/) ~~ A ) )
4 1 3 syl 
 |-  ( A e. V -> ( (/) ~< A <-> -. (/) ~~ A ) )
5 ensymb 
 |-  ( (/) ~~ A <-> A ~~ (/) )
6 en0 
 |-  ( A ~~ (/) <-> A = (/) )
7 5 6 bitri 
 |-  ( (/) ~~ A <-> A = (/) )
8 7 necon3bbii 
 |-  ( -. (/) ~~ A <-> A =/= (/) )
9 4 8 bitrdi 
 |-  ( A e. V -> ( (/) ~< A <-> A =/= (/) ) )