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	$⊢ X \in dom F \to F \neq \emptyset$

Step	Hyp	Ref	Expression
1		ne0i	$⊢ X \in dom F \to dom F \neq \emptyset$
2		dmeq	$⊢ F = \emptyset \to dom F = dom \emptyset$
3		dm0	$⊢ dom \emptyset = \emptyset$
4	2 3	eqtrdi	$⊢ F = \emptyset \to dom F = \emptyset$
5	4	necon3i	$⊢ dom F \neq \emptyset \to F \neq \emptyset$
6	1 5	syl	$⊢ X \in dom F \to F \neq \emptyset$