Theorem f1ofo 6779

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

Step	Hyp	Ref	Expression
1		dff1o3 6778	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 497	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)

Syntax hints:   → wi 4  ^◡ccnv 5621  Fun wfun 6484  –onto→wfo 6488  –1-1-onto→wf1o 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-cleq 2726  df-ss 3916  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497

This theorem is referenced by:  f1imacnv  6788  resin  6794  f1ococnv2  6799  fo00  6808  f1ounsn  7216  f1ocoima  7247  isoini  7282  isofrlem  7284  isoselem  7285  ncanth  7311  f1opw2  7611  f1dmex  7899  f1ovv  7900  f1oweALT  7914  wemoiso2  7916  mptcnfimad  7928  curry1  8044  curry2  8047  smoiso2  8299  f1osetex  8794  bren  8891  f1oeng  8905  en1  8959  canth2  9056  domss2  9062  mapen  9067  ssenen  9077  dif1enlem  9082  ssfiALT  9096  phplem2  9127  php3  9131  f1fi  9212  domunfican  9220  fiint  9225  f1opwfi  9254  mapfien  9309  supisolem  9375  ordiso2  9418  ordtypelem10  9430  oismo  9443  wdomref  9475  brwdom2  9476  unxpwdom2  9491  cantnflt2  9580  cantnfp1lem3  9587  wemapwe  9604  infxpenc2lem1  9927  fseqen  9935  infpwfien  9970  infmap2  10125  ackbij2  10150  cff1  10166  cofsmo  10177  infpssr  10216  enfin2i  10229  fin23lem27  10236  enfin1ai  10292  fin1a2lem7  10314  axcclem  10365  ttukeylem1  10417  fpwwe2lem5  10544  fpwwe2lem8  10547  canthp1lem2  10562  tskuni  10692  gruen  10721  cnexALT  12897  fiinfnf1o  14271  hasheqf1oi  14272  hashfacen  14375  fsumf1o  15644  fsumss  15646  fprodf1o  15867  fprodss  15869  ruc  16166  unbenlem  16834  xpsfrn  17487  xpsbas  17491  xpsadd  17493  xpsmul  17494  xpssca  17495  xpsvsca  17496  xpsless  17497  xpsle  17498  imasmndf1  18699  sursubmefmnd  18819  imasgrpf1  18985  gicsubgen  19206  symgmov2  19315  symgextfo  19349  symgfixelsi  19362  giccyg  19827  gsumzres  19836  gsumzcl2  19837  gsumzf1o  19839  gsumzaddlem  19848  gsumconst  19861  gsumzmhm  19864  gsumzoppg  19871  dprdf1o  19961  imasrngf1  20111  imasringf1  20265  gsumfsum  21387  znleval  21507  lmimlbs  21789  lbslcic  21794  coe1mul2lem2  22208  cmpfi  23350  idqtop  23648  basqtop  23653  tgqtop  23654  hmeontr  23711  hmeoimaf1o  23712  hmeoqtop  23717  cmphmph  23730  connhmph  23731  nrmhmph  23736  indishmph  23740  cmphaushmeo  23742  xpstps  23752  xpstopnlem2  23753  fmid  23902  tsmsf1o  24087  imasdsf1olem  24315  imasf1oxmet  24317  imasf1omet  24318  xpsdsfn  24319  imasf1oxms  24431  imasf1oms  24432  iccpnfhmeo  24897  cnheiborlem  24907  ovolctb  25445  ovolicc2lem4  25475  dyadmbl  25555  mbfimaopnlem  25610  itg1addlem4  25654  dvcnvrelem2  25977  dvcnvre  25978  deg1ldg  26051  deg1leb  26054  efifo  26510  logrn  26521  dvrelog  26600  efopnlem2  26620  fsumdvdsmul  27159  fsumdvdsmulOLD  27161  f1otrg  28892  axcontlem10  28995  edgusgrnbfin  29395  eupthvdres  30259  cnvunop  31942  counop  31945  idunop  32002  elunop2  32037  fmptco1f1o  32660  padct  32746  mndlactf1o  33061  mndractf1o  33062  symgcom  33114  cycpmconjvlem  33172  cycpmconjslem2  33186  1arithidomlem2  33566  esplysply  33678  xrge0iifiso  34041  volmeas  34337  ballotlemro  34629  derangenlem  35314  subfacp1lem3  35325  subfacp1lem5  35327  erdsze2lem1  35346  cvmsss2  35417  poimirlem1  37761  poimirlem2  37762  poimirlem3  37763  poimirlem4  37764  poimirlem5  37765  poimirlem6  37766  poimirlem7  37767  poimirlem9  37769  poimirlem10  37770  poimirlem11  37771  poimirlem12  37772  poimirlem14  37774  poimirlem15  37775  poimirlem16  37776  poimirlem17  37777  poimirlem19  37779  poimirlem20  37780  poimirlem22  37782  poimirlem23  37783  poimirlem24  37784  poimirlem25  37785  poimirlem29  37789  poimirlem31  37791  mblfinlem2  37798  ismtybndlem  37946  ismtyres  37948  diaintclN  41257  dibintclN  41366  mapdrn  41848  aks6d1c1p5  42305  riccrng1  42718  ricdrng1  42725  dnnumch2  43229  kelac1  43247  lnmlmic  43272  pwslnmlem1  43276  pwfi2f1o  43280  gicabl  43283  imasgim  43284  isnumbasgrplem1  43285  ntrneifv2  44263  stoweidlem27  46213  fourierdlem20  46313  fourierdlem51  46343  fourierdlem52  46344  fourierdlem63  46355  fourierdlem64  46356  fourierdlem65  46357  fourierdlem102  46394  fourierdlem114  46406  sge0f1o  46568  nnfoctbdjlem  46641  isomenndlem  46716  ovnsubaddlem1  46756  3f1oss1  47263  f1oresf1o2  47479  grimuhgr  48075  grimcnv  48076  isuspgrimlem  48083  grimedg  48123  isubgr3stgrlem8  48161  tposres3  49068  uptrlem1  49397  lmdran  49858  cmdlan  49859