Theorem fvmpt2bd

Description: Value of a function given by the maps-to notation. Deduction version. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypothesis	fvmpt2bd.1	|- ( ph -> F = ( x e. A |-> B ) )
Assertion	fvmpt2bd	|- ( ( ph /\ x e. A /\ B e. C ) -> ( F ` x ) = B )

Proof

Step	Hyp	Ref	Expression
1		fvmpt2bd.1	|- ( ph -> F = ( x e. A |-> B ) )
2	1	fveq1d	|- ( ph -> ( F ` x ) = ( ( x e. A |-> B ) ` x ) )
3	2	3ad2ant1	|- ( ( ph /\ x e. A /\ B e. C ) -> ( F ` x ) = ( ( x e. A |-> B ) ` x ) )
4		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
5	4	fvmpt2	|- ( ( x e. A /\ B e. C ) -> ( ( x e. A |-> B ) ` x ) = B )
6	5	3adant1	|- ( ( ph /\ x e. A /\ B e. C ) -> ( ( x e. A |-> B ) ` x ) = B )
7	3 6	eqtrd	|- ( ( ph /\ x e. A /\ B e. C ) -> ( F ` x ) = B )