Theorem dfatelrn

Description: The value of a function F at a set A is in the range of the function F if F is defined at A . (Contributed by AV, 1-Sep-2022)

	Ref	Expression
Assertion	dfatelrn	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		df-dfat	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
2		funressndmfvrn	⊢ ( ( Fun ( 𝐹 ↾ { 𝐴 } ) ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )
3	2	ancoms	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )
4	1 3	sylbi	⊢ ( 𝐹 defAt 𝐴 → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )