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

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

Proof of Theorem foeq3
StepHypRef Expression
1 eqeq2 2472 . . 3
21anbi2d 703 . 2
3 df-fo 5599 . 2
4 df-fo 5599 . 2
52, 3, 43bitr4g 288 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  rancrn 5005  Fnwfn 5588  -onto->wfo 5591 This theorem is referenced by:  f1oeq3  5814  foeq123d  5817  resdif  5841  ffoss  6761  fidomdm  7822  fifo  7912  brwdom  8014  brwdom2  8020  canthwdom  8026  ixpiunwdom  8038  fin1a2lem7  8807  znnen  13946  quslem  14940  znzrhfo  18586  rncmp  19896  conima  19926  concn  19927  qtopcmplem  20208  qtoprest  20218  opidon2OLD  25326  pjhfo  26624  dmct  27537  msrfo  28906  ivthALT  30153 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449  df-fo 5599
 Copyright terms: Public domain W3C validator