Metamath Proof Explorer


Theorem fvmpt4

Description: Value of a function given by the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion fvmpt4
|- ( ( x e. A /\ B e. C ) -> ( ( x e. A |-> B ) ` x ) = B )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
2 1 fvmpt2
 |-  ( ( x e. A /\ B e. C ) -> ( ( x e. A |-> B ) ` x ) = B )