Theorem fvmap

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

	Ref	Expression
Hypotheses	fvmap.a	$$⊢\phi \to A\in V$$
	fvmap.b	$$⊢\phi \to B\in W$$
	fvmap.f	$$⊢\phi \to F\in \left(A^B\right)$$
	fvmap.c	$$⊢\phi \to C\in B$$
Assertion	fvmap	$$⊢\phi \to F\left(C\right)\in A$$

Proof

Step	Hyp	Ref	Expression
1		fvmap.a	$$⊢\phi \to A\in V$$
2		fvmap.b	$$⊢\phi \to B\in W$$
3		fvmap.f	$$⊢\phi \to F\in \left(A^B\right)$$
4		fvmap.c	$$⊢\phi \to C\in B$$
5		id	$$⊢\phi \to \phi$$
6		elmapg	$$⊢\left(A\in V\wedge B\in W\right)\to \left(F\in \left(A^B\right)\leftrightarrow F:B⟶A\right)$$
7	1 2 6	syl2anc	$$⊢\phi \to \left(F\in \left(A^B\right)\leftrightarrow F:B⟶A\right)$$
8	3 7	mpbid	$$⊢\phi \to F:B⟶A$$
9	8	ffvelrnda	$$⊢\left(\phi \wedge C\in B\right)\to F\left(C\right)\in A$$
10	5 4 9	syl2anc	$$⊢\phi \to F\left(C\right)\in A$$