Metamath Proof Explorer


Theorem foeq1

Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion foeq1 F=GF:AontoBG:AontoB

Proof

Step Hyp Ref Expression
1 fneq1 F=GFFnAGFnA
2 rneq F=GranF=ranG
3 2 eqeq1d F=GranF=BranG=B
4 1 3 anbi12d F=GFFnAranF=BGFnAranG=B
5 df-fo F:AontoBFFnAranF=B
6 df-fo G:AontoBGFnAranG=B
7 4 5 6 3bitr4g F=GF:AontoBG:AontoB