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 )