Metamath Proof Explorer


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 )