This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eldmne0

Description: A function of nonempty domain is not empty. (Contributed by Thierry Arnoux, 20-Nov-2023)

Ref Expression
Assertion eldmne0 ( 𝑋 ∈ dom 𝐹 → 𝐹 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 ne0i ⊢ ( 𝑋 ∈ dom 𝐹 → dom 𝐹 ≠ ∅ )
2 dmeq ⊢ ( 𝐹 = ∅ → dom 𝐹 = dom ∅ )
3 dm0 ⊢ dom ∅ = ∅
4 2 3 eqtrdi ⊢ ( 𝐹 = ∅ → dom 𝐹 = ∅ )
5 4 necon3i ⊢ ( dom 𝐹 ≠ ∅ → 𝐹 ≠ ∅ )
6 1 5 syl ⊢ ( 𝑋 ∈ dom 𝐹 → 𝐹 ≠ ∅ )