Metamath Proof Explorer

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	$⊢ F defAt A \to F (A) \in ran F$

Step	Hyp	Ref	Expression
1		df-dfat	$⊢ F defAt A \leftrightarrow (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
2		funressndmfvrn	$⊢ (Fun ({F ↾}_{\{A\}}) \land A \in dom F) \to F (A) \in ran F$
3	2	ancoms	$⊢ (A \in dom F \land Fun ({F ↾}_{\{A\}})) \to F (A) \in ran F$
4	1 3	sylbi	$⊢ F defAt A \to F (A) \in ran F$