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 
|- ( ( F Fn A /\ X e. A ) -> ( `' F " { ( F ` X ) } ) =/= (/) )

Proof

Step Hyp Ref Expression
1 preimafvsnel 
 |-  ( ( F Fn A /\ X e. A ) -> X e. ( `' F " { ( F ` X ) } ) )
2 1 ne0d 
 |-  ( ( F Fn A /\ X e. A ) -> ( `' F " { ( F ` X ) } ) =/= (/) )