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
|- ( ph -> F Fn A )
fnfvelrnd.2
|- ( ph -> B e. A )
Assertion fnfvelrnd
|- ( ph -> ( F ` B ) e. ran F )

Proof

Step Hyp Ref Expression
1 fnfvelrnd.1
 |-  ( ph -> F Fn A )
2 fnfvelrnd.2
 |-  ( ph -> B e. A )
3 fnfvelrn
 |-  ( ( F Fn A /\ B e. A ) -> ( F ` B ) e. ran F )
4 1 2 3 syl2anc
 |-  ( ph -> ( F ` B ) e. ran F )