MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1ofo Structured version   Visualization version   GIF version

Theorem f1ofo 6604
Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)
Assertion
Ref Expression
f1ofo (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)

Proof of Theorem f1ofo
StepHypRef Expression
1 dff1o3 6603 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
21simplbi 501 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ccnv 5531  Fun wfun 6328  ontowfo 6332  1-1-ontowf1o 6333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-v 3471  df-in 3915  df-ss 3925  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341
This theorem is referenced by:  f1imacnv  6613  resin  6618  f1ococnv2  6623  fo00  6632  isoini  7075  isofrlem  7077  isoselem  7078  ncanth  7096  f1opw2  7385  f1dmex  7644  f1ovv  7645  f1oweALT  7659  wemoiso2  7661  curry1  7786  curry2  7789  smoiso2  7993  bren  8505  f1oeng  8515  en1  8563  canth2  8658  domss2  8664  mapen  8669  ssenen  8679  phplem4  8687  php3  8691  ssfi  8726  domunfican  8779  fiint  8783  f1fi  8799  f1opwfi  8816  mapfien  8859  supisolem  8925  ordiso2  8967  ordtypelem10  8979  oismo  8992  wdomref  9024  brwdom2  9025  unxpwdom2  9040  cantnflt2  9124  cantnfp1lem3  9131  wemapwe  9148  infxpenc2lem1  9434  fseqen  9442  infpwfien  9477  infmap2  9629  ackbij2  9654  cff1  9669  cofsmo  9680  infpssr  9719  enfin2i  9732  fin23lem27  9739  enfin1ai  9795  fin1a2lem7  9817  axcclem  9868  ttukeylem1  9920  fpwwe2lem6  10046  fpwwe2lem9  10049  canthp1lem2  10064  tskuni  10194  gruen  10223  cnexALT  12373  fiinfnf1o  13706  hasheqf1oi  13708  hashfacen  13808  fsumf1o  15071  fsumss  15073  fprodf1o  15291  fprodss  15293  ruc  15587  unbenlem  16233  xpsfrn  16832  xpsbas  16836  xpsadd  16838  xpsmul  16839  xpssca  16840  xpsvsca  16841  xpsless  16842  xpsle  16843  imasmndf1  17941  sursubmefmnd  18052  imasgrpf1  18207  gicsubgen  18409  symgmov2  18507  symgextfo  18541  symgfixelsi  18554  giccyg  19011  gsumzres  19020  gsumzcl2  19021  gsumzf1o  19023  gsumzaddlem  19032  gsumconst  19045  gsumzmhm  19048  gsumzoppg  19055  dprdf1o  19145  gsumfsum  20156  znleval  20244  lmimlbs  20523  lbslcic  20528  coe1mul2lem2  20895  cmpfi  22011  idqtop  22309  basqtop  22314  tgqtop  22315  hmeontr  22372  hmeoimaf1o  22373  hmeoqtop  22378  cmphmph  22391  connhmph  22392  nrmhmph  22397  indishmph  22401  cmphaushmeo  22403  xpstps  22413  xpstopnlem2  22414  fmid  22563  tsmsf1o  22748  imasdsf1olem  22978  imasf1oxmet  22980  imasf1omet  22981  xpsdsfn  22982  imasf1oxms  23094  imasf1oms  23095  iccpnfhmeo  23548  cnheiborlem  23557  ovolctb  24092  ovolicc2lem4  24122  dyadmbl  24202  mbfimaopnlem  24257  itg1addlem4  24301  dvcnvrelem2  24619  dvcnvre  24620  deg1ldg  24691  deg1leb  24694  efifo  25137  logrn  25148  dvrelog  25226  efopnlem2  25246  fsumdvdsmul  25778  f1otrg  26663  axcontlem10  26765  edgusgrnbfin  27161  eupthvdres  28018  cnvunop  29699  counop  29702  idunop  29759  elunop2  29794  fmptco1f1o  30386  padct  30465  symgcom  30758  cycpmconjvlem  30814  cycpmconjslem2  30828  xrge0iifiso  31252  volmeas  31564  ballotlemro  31854  derangenlem  32492  subfacp1lem3  32503  subfacp1lem5  32505  erdsze2lem1  32524  cvmsss2  32595  poimirlem1  35020  poimirlem2  35021  poimirlem3  35022  poimirlem4  35023  poimirlem5  35024  poimirlem6  35025  poimirlem7  35026  poimirlem9  35028  poimirlem10  35029  poimirlem11  35030  poimirlem12  35031  poimirlem14  35033  poimirlem15  35034  poimirlem16  35035  poimirlem17  35036  poimirlem19  35038  poimirlem20  35039  poimirlem22  35041  poimirlem23  35042  poimirlem24  35043  poimirlem25  35044  poimirlem29  35048  poimirlem31  35050  mblfinlem2  35057  ismtybndlem  35206  ismtyres  35208  diaintclN  38316  dibintclN  38425  mapdrn  38907  dnnumch2  39923  kelac1  39941  lnmlmic  39966  pwslnmlem1  39970  pwfi2f1o  39974  gicabl  39977  imasgim  39978  isnumbasgrplem1  39979  ntrneifv2  40720  stoweidlem27  42612  fourierdlem20  42712  fourierdlem51  42742  fourierdlem52  42743  fourierdlem63  42754  fourierdlem64  42755  fourierdlem65  42756  fourierdlem102  42793  fourierdlem114  42805  sge0f1o  42964  nnfoctbdjlem  43037  isomenndlem  43112  ovnsubaddlem1  43152  f1oresf1o2  43790  isomuspgrlem2d  44292
  Copyright terms: Public domain W3C validator