Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  foeq3 Structured version   Unicode version

Theorem foeq3 5643
 Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
foeq3

Proof of Theorem foeq3
StepHypRef Expression
1 eqeq2 2444 . . 3
21anbi2d 685 . 2
3 df-fo 5452 . 2
4 df-fo 5452 . 2
52, 3, 43bitr4g 280 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1652   crn 4871   wfn 5441  wfo 5444 This theorem is referenced by:  f1oeq3  5659  foeq123d  5662  resdif  5688  ffoss  5699  fidomdm  7380  fifo  7429  brwdom  7527  brwdom2  7533  canthwdom  7539  ixpiunwdom  7551  fin1a2lem7  8278  znnen  12804  divslem  13760  znzrhfo  16820  rncmp  17451  conima  17480  concn  17481  qtopcmplem  17731  qtoprest  17741  opidon2  21904  pjhfo  23200  dmct  24098  ivthALT  26329 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-fo 5452
 Copyright terms: Public domain W3C validator