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

Theorem f1oeq3 5814
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1oeq3

Proof of Theorem f1oeq3
StepHypRef Expression
1 f1eq3 5783 . . 3
2 foeq3 5798 . . 3
31, 2anbi12d 710 . 2
4 df-f1o 5600 . 2
5 df-f1o 5600 . 2
63, 4, 53bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  -1-1->wf1 5590  -onto->wfo 5591  -1-1-onto->wf1o 5592
This theorem is referenced by:  f1oeq23  5815  f1oeq123d  5818  f1ores  5835  resdif  5841  resin  5842  f1osng  5859  f1oresrab  6063  fveqf1o  6205  isoeq5  6219  isoini2  6235  ncanth  6255  oacomf1o  7233  mapsnf1o  7530  bren  7545  xpcomf1o  7626  domss2  7696  isinf  7753  wemapwe  8160  wemapweOLD  8161  oef1o  8162  oef1oOLD  8163  cnfcomlem  8164  cnfcom2  8167  cnfcom3  8169  cnfcom3clem  8170  cnfcomlemOLD  8172  cnfcom2OLD  8175  cnfcom3OLD  8177  cnfcom3clemOLD  8178  infxpenc  8416  infxpenc2lem1  8417  infxpenc2  8420  infxpencOLD  8421  infxpenc2OLD  8424  ackbij2lem2  8641  fin1a2lem6  8806  hsmexlem1  8827  pwfseqlem5  9062  pwfseq  9063  hashgf1o  12081  axdc4uzlem  12092  sumeq1  13511  fsumss  13547  fsumcnv  13588  prodeq1f  13715  fprodss  13755  fprodcnv  13787  unbenlem  14426  4sqlem11  14473  pwssnf1o  14895  catcisolem  15433  yoniso  15554  gsumvalx  15897  gsumpropd  15899  gsumpropd2lem  15900  xpsmnd  15960  xpsgrp  16189  cayley  16439  cayleyth  16440  gsumval3OLD  16908  gsumval3lem1  16909  gsumval3lem2  16910  gsumcom2  17003  coe1mul2lem2  18309  scmatrngiso  19038  m2cpmrngiso  19259  cncfcnvcn  21425  ovolicc2lem4  21931  logf1o2  23031  uslgraf1oedg  24359  clwwlkvbij  24801  iseupa  24965  adjbd1o  27004  rinvf1o  27472  eulerpartgbij  28311  eulerpartlemgh  28317  derangval  28611  subfacp1lem2a  28624  subfacp1lem3  28626  subfacp1lem5  28628  mrsubff1o  28875  msubff1o  28917  elgiso  29036  ismtyval  30296  ismrer1  30334  rngoisoval  30380  pwfi2f1o  31044  imasgim  31048  equivestrcsetc  32658  bj-finsumval0  34663  lautset  35806  pautsetN  35822  hvmap1o2  37492
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-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600
  Copyright terms: Public domain W3C validator