This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvn0fvelrn

Description: If the value of a function is not null, the value is an element of the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Proof shortened by SN, 13-Jan-2025)

Ref Expression
Assertion fvn0fvelrn ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 fvrn0 ⊢ ( 𝐹 ‘ 𝑋 ) ∈ ( ran 𝐹 ∪ { ∅ } )
2 nelsn ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → ¬ ( 𝐹 ‘ 𝑋 ) ∈ { ∅ } )
3 elunnel2 ⊢ ( ( ( 𝐹 ‘ 𝑋 ) ∈ ( ran 𝐹 ∪ { ∅ } ) ∧ ¬ ( 𝐹 ‘ 𝑋 ) ∈ { ∅ } ) → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 )
4 1 2 3 sylancr ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 )