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 ( ( 𝑥𝐴𝐵𝐶 ) → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
2 1 fvmpt2 ( ( 𝑥𝐴𝐵𝐶 ) → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) = 𝐵 )