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	⊢ ( 𝐴 ∈ ( 𝐹 ‘ 𝐵 ) → 𝐹 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		ne0i	⊢ ( 𝐴 ∈ ( 𝐹 ‘ 𝐵 ) → ( 𝐹 ‘ 𝐵 ) ≠ ∅ )
2		fveq1	⊢ ( 𝐹 = ∅ → ( 𝐹 ‘ 𝐵 ) = ( ∅ ‘ 𝐵 ) )
3		0fv	⊢ ( ∅ ‘ 𝐵 ) = ∅
4	2 3	eqtrdi	⊢ ( 𝐹 = ∅ → ( 𝐹 ‘ 𝐵 ) = ∅ )
5	4	necon3i	⊢ ( ( 𝐹 ‘ 𝐵 ) ≠ ∅ → 𝐹 ≠ ∅ )
6	1 5	syl	⊢ ( 𝐴 ∈ ( 𝐹 ‘ 𝐵 ) → 𝐹 ≠ ∅ )