Description: A function's value belongs to its range. (Contributed by NM, 15-Oct-1996)
Ref | Expression | ||
---|---|---|---|
Assertion | fnfvelrn | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ ran 𝐹 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvelrn | ⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐵 ) ∈ ran 𝐹 ) | |
2 | 1 | funfni | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ ran 𝐹 ) |