Theorem 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 /\ A e. dom F ) -> ( F ''' A ) e. ran F )

Proof

Step	Hyp	Ref	Expression
1		funres	|- ( Fun F -> Fun ( F |` { A } ) )
2	1	anim1i	|- ( ( Fun F /\ A e. dom F ) -> ( Fun ( F |` { A } ) /\ A e. dom F ) )
3	2	ancomd	|- ( ( Fun F /\ A e. dom F ) -> ( A e. dom F /\ Fun ( F |` { A } ) ) )
4		df-dfat	|- ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
5	3 4	sylibr	|- ( ( Fun F /\ A e. dom F ) -> F defAt A )
6		afvfundmfveq	|- ( F defAt A -> ( F ''' A ) = ( F ` A ) )
7	6	eqcomd	|- ( F defAt A -> ( F ` A ) = ( F ''' A ) )
8	5 7	syl	|- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) = ( F ''' A ) )
9		fvelrn	|- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F )
10	8 9	eqeltrrd	|- ( ( Fun F /\ A e. dom F ) -> ( F ''' A ) e. ran F )