Description: Any set dominates the empty set. (Contributed by NM, 26-Oct-2003) (Revised by Mario Carneiro, 26-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | 0domg | ⊢ ( 𝐴 ∈ 𝑉 → ∅ ≼ 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ss | ⊢ ∅ ⊆ 𝐴 | |
2 | ssdomg | ⊢ ( 𝐴 ∈ 𝑉 → ( ∅ ⊆ 𝐴 → ∅ ≼ 𝐴 ) ) | |
3 | 1 2 | mpi | ⊢ ( 𝐴 ∈ 𝑉 → ∅ ≼ 𝐴 ) |