Metamath Proof Explorer
Description: An alternate function value belongs to the range of the function,
analogous to fnfvelrn . (Contributed by AV, 2-Sep-2022)
|
|
Ref |
Expression |
|
Assertion |
fnafv2elrn |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 '''' 𝐵 ) ∈ ran 𝐹 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
afv2elrn |
⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹 ) → ( 𝐹 '''' 𝐵 ) ∈ ran 𝐹 ) |
2 |
1
|
funfni |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 '''' 𝐵 ) ∈ ran 𝐹 ) |