Metamath Proof Explorer


Theorem feq12d

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

Ref Expression
Hypotheses feq12d.1 φ F = G
feq12d.2 φ A = B
Assertion feq12d φ F : A C G : B C

Proof

Step Hyp Ref Expression
1 feq12d.1 φ F = G
2 feq12d.2 φ A = B
3 1 feq1d φ F : A C G : A C
4 2 feq2d φ G : A C G : B C
5 3 4 bitrd φ F : A C G : B C