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 ^m B )
	mapfvd.f	|- ( ph -> F e. M )
	mapfvd.x	|- ( ph -> X e. B )
Assertion	mapfvd	|- ( ph -> ( F ` X ) e. A )

Proof

Step	Hyp	Ref	Expression
1		mapfvd.m	|- M = ( A ^m B )
2		mapfvd.f	|- ( ph -> F e. M )
3		mapfvd.x	|- ( ph -> X e. B )
4		elmapi	|- ( F e. ( A ^m B ) -> F : B --> A )
5		ffvelrn	|- ( ( F : B --> A /\ X e. B ) -> ( F ` X ) e. A )
6	5	expcom	|- ( X e. B -> ( F : B --> A -> ( F ` X ) e. A ) )
7	3 4 6	syl2imc	|- ( F e. ( A ^m B ) -> ( ph -> ( F ` X ) e. A ) )
8	7 1	eleq2s	|- ( F e. M -> ( ph -> ( F ` X ) e. A ) )
9	2 8	mpcom	|- ( ph -> ( F ` X ) e. A )