Metamath Proof Explorer


Theorem 0sdom

Description: A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 29-Jul-2004)

Ref Expression
Hypothesis 0sdom.1 𝐴 ∈ V
Assertion 0sdom ( ∅ ≺ 𝐴𝐴 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 0sdom.1 𝐴 ∈ V
2 0sdomg ( 𝐴 ∈ V → ( ∅ ≺ 𝐴𝐴 ≠ ∅ ) )
3 1 2 ax-mp ( ∅ ≺ 𝐴𝐴 ≠ ∅ )