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

Metamath Proof Explorer

Theorem elfvne0

Description: If a function value has a member, then the function is not an empty set (An artifact of our function value definition.) (Contributed by Zhi Wang, 16-Sep-2024)

		Ref	Expression
	Assertion	elfvne0	$⊢ A \in F (B) \to F \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$⊢ A \in F (B) \to F (B) \neq \emptyset$
2		fveq1	$⊢ F = \emptyset \to F (B) = \emptyset (B)$
3		0fv	$⊢ \emptyset (B) = \emptyset$
4	2 3	eqtrdi	$⊢ F = \emptyset \to F (B) = \emptyset$
5	4	necon3i	$⊢ F (B) \neq \emptyset \to F \neq \emptyset$
6	1 5	syl	$⊢ A \in F (B) \to F \neq \emptyset$