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 ( 𝜑𝐹 = ( 𝑥𝐴𝐵 ) )
Assertion fvmpt2bd ( ( 𝜑𝑥𝐴𝐵𝐶 ) → ( 𝐹𝑥 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 fvmpt2bd.1 ( 𝜑𝐹 = ( 𝑥𝐴𝐵 ) )
2 1 fveq1d ( 𝜑 → ( 𝐹𝑥 ) = ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) )
3 2 3ad2ant1 ( ( 𝜑𝑥𝐴𝐵𝐶 ) → ( 𝐹𝑥 ) = ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) )
4 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
5 4 fvmpt2 ( ( 𝑥𝐴𝐵𝐶 ) → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) = 𝐵 )
6 5 3adant1 ( ( 𝜑𝑥𝐴𝐵𝐶 ) → ( ( 𝑥𝐴𝐵 ) ‘ 𝑥 ) = 𝐵 )
7 3 6 eqtrd ( ( 𝜑𝑥𝐴𝐵𝐶 ) → ( 𝐹𝑥 ) = 𝐵 )