Metamath Proof Explorer


Theorem preimafvn0

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

Ref Expression
Assertion preimafvn0 FFnAXAF-1FX

Proof

Step Hyp Ref Expression
1 preimafvsnel FFnAXAXF-1FX
2 1 ne0d FFnAXAF-1FX