Theorem mapfvd

Description: The value of a function that maps from B to A . (Contributed by AV, 2-Feb-2023)

	Ref	Expression
Hypotheses	mapfvd.m	$$⊢M=A^B$$
	mapfvd.f	$$⊢\phi \to F\in M$$
	mapfvd.x	$$⊢\phi \to X\in B$$
Assertion	mapfvd	$$⊢\phi \to F\left(X\right)\in A$$

Proof

Step	Hyp	Ref	Expression
1		mapfvd.m	$$⊢M=A^B$$
2		mapfvd.f	$$⊢\phi \to F\in M$$
3		mapfvd.x	$$⊢\phi \to X\in B$$
4		elmapi	$$⊢F\in \left(A^B\right)\to F:B⟶A$$
5		ffvelcdm	$$⊢\left(F:B⟶A\wedge X\in B\right)\to F\left(X\right)\in A$$
6	5	expcom	$$⊢X\in B\to \left(F:B⟶A\to F\left(X\right)\in A\right)$$
7	3 4 6	syl2imc	$$⊢F\in \left(A^B\right)\to \left(\phi \to F\left(X\right)\in A\right)$$
8	7 1	eleq2s	$$⊢F\in M\to \left(\phi \to F\left(X\right)\in A\right)$$
9	2 8	mpcom	$$⊢\phi \to F\left(X\right)\in A$$