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 𝐹 → 𝐹 ≠ ∅ )