Metamath Proof Explorer


Theorem feq1dd

Description: Equality deduction for functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses feq1dd.eq φF=G
feq1dd.f φF:AB
Assertion feq1dd φG:AB

Proof

Step Hyp Ref Expression
1 feq1dd.eq φF=G
2 feq1dd.f φF:AB
3 1 feq1d φF:ABG:AB
4 2 3 mpbid φG:AB