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\left(B\right)\to F\ne \varnothing$$

Proof

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