Theorem fvmap

Description: Function value for a member of a set exponentiation. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	fvmap.a	|- ( ph -> A e. V )
	fvmap.b	|- ( ph -> B e. W )
	fvmap.f	|- ( ph -> F e. ( A ^m B ) )
	fvmap.c	|- ( ph -> C e. B )
Assertion	fvmap	|- ( ph -> ( F ` C ) e. A )

Proof

Step	Hyp	Ref	Expression
1		fvmap.a	|- ( ph -> A e. V )
2		fvmap.b	|- ( ph -> B e. W )
3		fvmap.f	|- ( ph -> F e. ( A ^m B ) )
4		fvmap.c	|- ( ph -> C e. B )
5		id	|- ( ph -> ph )
6		elmapg	|- ( ( A e. V /\ B e. W ) -> ( F e. ( A ^m B ) <-> F : B --> A ) )
7	1 2 6	syl2anc	|- ( ph -> ( F e. ( A ^m B ) <-> F : B --> A ) )
8	3 7	mpbid	|- ( ph -> F : B --> A )
9	8	ffvelrnda	|- ( ( ph /\ C e. B ) -> ( F ` C ) e. A )
10	5 4 9	syl2anc	|- ( ph -> ( F ` C ) e. A )