Metamath Proof Explorer


Theorem fnfvelrnd

Description: A function's value belongs to its range. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses fnfvelrnd.1 ( 𝜑𝐹 Fn 𝐴 )
fnfvelrnd.2 ( 𝜑𝐵𝐴 )
Assertion fnfvelrnd ( 𝜑 → ( 𝐹𝐵 ) ∈ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 fnfvelrnd.1 ( 𝜑𝐹 Fn 𝐴 )
2 fnfvelrnd.2 ( 𝜑𝐵𝐴 )
3 fnfvelrn ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( 𝐹𝐵 ) ∈ ran 𝐹 )
4 1 2 3 syl2anc ( 𝜑 → ( 𝐹𝐵 ) ∈ ran 𝐹 )