Metamath Proof Explorer

Theorem 0domg

Description: Any set dominates the empty set. (Contributed by NM, 26-Oct-2003) (Revised by Mario Carneiro, 26-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ A
2 ssdomg 
 |-  ( A e. V -> ( (/) C_ A -> (/) ~<_ A ) )
3 1 2 mpi 
 |-  ( A e. V -> (/) ~<_ A )