Metamath Proof Explorer


Theorem feq12d

Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Hypotheses feq12d.1 ( 𝜑𝐹 = 𝐺 )
feq12d.2 ( 𝜑𝐴 = 𝐵 )
Assertion feq12d ( 𝜑 → ( 𝐹 : 𝐴𝐶𝐺 : 𝐵𝐶 ) )

Proof

Step Hyp Ref Expression
1 feq12d.1 ( 𝜑𝐹 = 𝐺 )
2 feq12d.2 ( 𝜑𝐴 = 𝐵 )
3 1 feq1d ( 𝜑 → ( 𝐹 : 𝐴𝐶𝐺 : 𝐴𝐶 ) )
4 2 feq2d ( 𝜑 → ( 𝐺 : 𝐴𝐶𝐺 : 𝐵𝐶 ) )
5 3 4 bitrd ( 𝜑 → ( 𝐹 : 𝐴𝐶𝐺 : 𝐵𝐶 ) )