afvelrn

Description: A function's value belongs to its range, analogous to fvelrn . (Contributed by Alexander van der Vekens, 25-May-2017)

		Ref	Expression
	Assertion	afvelrn	$⊢ (Fun F \land A \in dom F) \to (F''' A) \in ran F$

Step	Hyp	Ref	Expression
1		funres	$⊢ Fun F \to Fun ({F ↾}_{\{A\}})$
2	1	anim1i	$⊢ (Fun F \land A \in dom F) \to (Fun ({F ↾}_{\{A\}}) \land A \in dom F)$
3	2	ancomd	$⊢ (Fun F \land A \in dom F) \to (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
4		df-dfat	$⊢ F defAt A \leftrightarrow (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
5	3 4	sylibr	$⊢ (Fun F \land A \in dom F) \to F defAt A$
6		afvfundmfveq	$⊢ F defAt A \to (F''' A) = F (A)$
7	6	eqcomd	$⊢ F defAt A \to F (A) = (F''' A)$
8	5 7	syl	$⊢ (Fun F \land A \in dom F) \to F (A) = (F''' A)$
9		fvelrn	$⊢ (Fun F \land A \in dom F) \to F (A) \in ran F$
10	8 9	eqeltrrd	$⊢ (Fun F \land A \in dom F) \to (F''' A) \in ran F$

Metamath Proof Explorer