Metamath Proof Explorer
Description: A function's value belongs to its range. (Contributed by NM, 15Oct1996)


Ref 
Expression 

Assertion 
fnfvelrn 
$${\u22a2}\left({F}Fn{A}\wedge {B}\in {A}\right)\to {F}\left({B}\right)\in \mathrm{ran}{F}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

fvelrn 
$${\u22a2}\left(\mathrm{Fun}{F}\wedge {B}\in \mathrm{dom}{F}\right)\to {F}\left({B}\right)\in \mathrm{ran}{F}$$ 
2 
1

funfni 
$${\u22a2}\left({F}Fn{A}\wedge {B}\in {A}\right)\to {F}\left({B}\right)\in \mathrm{ran}{F}$$ 