Theorem eldmne0

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

	Ref	Expression
Assertion	eldmne0	$$⊢X\in \mathrm{dom}F\to F\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$$⊢X\in \mathrm{dom}F\to \mathrm{dom}F\ne \varnothing$$
2		dmeq	$$⊢F=\varnothing \to \mathrm{dom}F=\mathrm{dom}\varnothing$$
3		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
4	2 3	eqtrdi	$$⊢F=\varnothing \to \mathrm{dom}F=\varnothing$$
5	4	necon3i	$$⊢\mathrm{dom}F\ne \varnothing \to F\ne \varnothing$$
6	1 5	syl	$$⊢X\in \mathrm{dom}F\to F\ne \varnothing$$