Metamath Proof Explorer


Theorem 0dom

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

Ref Expression
Hypothesis 0sdom.1 ⊢ A ∈ V
Assertion 0dom ⊢ ∅ ≼ A

Proof

Step Hyp Ref Expression
1 0sdom.1 ⊢ A ∈ V
2 0domg ⊢ A ∈ V → ∅ ≼ A
3 1 2 ax-mp ⊢ ∅ ≼ A