Theorem preimafvn0

Description: The preimage of a function value is not empty. (Contributed by AV, 7-Mar-2024)

	Ref	Expression
Assertion	preimafvn0	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		preimafvsnel	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) )
2	1	ne0d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ≠ ∅ )