Theorem f1ofo 6782

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 6781	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 496	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)

Syntax hints:   → wi 4  ^◡ccnv 5624  Fun wfun 6487  –onto→wfo 6491  –1-1-onto→wf1o 6492

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-cleq 2729  df-ss 3907  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500

This theorem is referenced by:  f1imacnv  6791  resin  6797  f1ococnv2  6802  fo00  6811  f1ounsn  7221  f1ocoima  7252  isoini  7287  isofrlem  7289  isoselem  7290  ncanth  7316  f1opw2  7616  f1dmex  7904  f1ovv  7905  f1oweALT  7919  wemoiso2  7921  mptcnfimad  7933  curry1  8048  curry2  8051  smoiso2  8303  f1osetex  8800  bren  8897  f1oeng  8911  en1  8965  canth2  9062  domss2  9068  mapen  9073  ssenen  9083  dif1enlem  9088  ssfiALT  9102  phplem2  9133  php3  9137  f1fi  9218  domunfican  9226  fiint  9231  f1opwfi  9260  mapfien  9315  supisolem  9381  ordiso2  9424  ordtypelem10  9436  oismo  9449  wdomref  9481  brwdom2  9482  unxpwdom2  9497  cantnflt2  9588  cantnfp1lem3  9595  wemapwe  9612  infxpenc2lem1  9935  fseqen  9943  infpwfien  9978  infmap2  10133  ackbij2  10158  cff1  10174  cofsmo  10185  infpssr  10224  enfin2i  10237  fin23lem27  10244  enfin1ai  10300  fin1a2lem7  10322  axcclem  10373  ttukeylem1  10425  fpwwe2lem5  10552  fpwwe2lem8  10555  canthp1lem2  10570  tskuni  10700  gruen  10729  cnexALT  12930  fiinfnf1o  14306  hasheqf1oi  14307  hashfacen  14410  fsumf1o  15679  fsumss  15681  fprodf1o  15905  fprodss  15907  ruc  16204  unbenlem  16873  xpsfrn  17526  xpsbas  17530  xpsadd  17532  xpsmul  17533  xpssca  17534  xpsvsca  17535  xpsless  17536  xpsle  17537  imasmndf1  18738  sursubmefmnd  18858  imasgrpf1  19027  gicsubgen  19248  symgmov2  19357  symgextfo  19391  symgfixelsi  19404  giccyg  19869  gsumzres  19878  gsumzcl2  19879  gsumzf1o  19881  gsumzaddlem  19890  gsumconst  19903  gsumzmhm  19906  gsumzoppg  19913  dprdf1o  20003  imasrngf1  20153  imasringf1  20305  gsumfsum  21427  znleval  21547  lmimlbs  21829  lbslcic  21834  coe1mul2lem2  22246  cmpfi  23386  idqtop  23684  basqtop  23689  tgqtop  23690  hmeontr  23747  hmeoimaf1o  23748  hmeoqtop  23753  cmphmph  23766  connhmph  23767  nrmhmph  23772  indishmph  23776  cmphaushmeo  23778  xpstps  23788  xpstopnlem2  23789  fmid  23938  tsmsf1o  24123  imasdsf1olem  24351  imasf1oxmet  24353  imasf1omet  24354  xpsdsfn  24355  imasf1oxms  24467  imasf1oms  24468  iccpnfhmeo  24925  cnheiborlem  24934  ovolctb  25470  ovolicc2lem4  25500  dyadmbl  25580  mbfimaopnlem  25635  itg1addlem4  25679  dvcnvrelem2  25998  dvcnvre  25999  deg1ldg  26070  deg1leb  26073  efifo  26527  logrn  26538  dvrelog  26617  efopnlem2  26637  fsumdvdsmul  27175  f1otrg  28956  axcontlem10  29059  edgusgrnbfin  29459  eupthvdres  30323  cnvunop  32007  counop  32010  idunop  32067  elunop2  32102  fmptco1f1o  32724  padct  32809  mndlactf1o  33108  mndractf1o  33109  symgcom  33162  cycpmconjvlem  33220  cycpmconjslem2  33234  1arithidomlem2  33614  esplysply  33733  xrge0iifiso  34098  volmeas  34394  ballotlemro  34686  derangenlem  35372  subfacp1lem3  35383  subfacp1lem5  35385  erdsze2lem1  35404  cvmsss2  35475  poimirlem1  37959  poimirlem2  37960  poimirlem3  37961  poimirlem4  37962  poimirlem5  37963  poimirlem6  37964  poimirlem7  37965  poimirlem9  37967  poimirlem10  37968  poimirlem11  37969  poimirlem12  37970  poimirlem14  37972  poimirlem15  37973  poimirlem16  37974  poimirlem17  37975  poimirlem19  37977  poimirlem20  37978  poimirlem22  37980  poimirlem23  37981  poimirlem24  37982  poimirlem25  37983  poimirlem29  37987  poimirlem31  37989  mblfinlem2  37996  ismtybndlem  38144  ismtyres  38146  diaintclN  41521  dibintclN  41630  mapdrn  42112  aks6d1c1p5  42568  riccrng1  42983  ricdrng1  42990  dnnumch2  43494  kelac1  43512  lnmlmic  43537  pwslnmlem1  43541  pwfi2f1o  43545  gicabl  43548  imasgim  43549  isnumbasgrplem1  43550  ntrneifv2  44528  stoweidlem27  46476  fourierdlem20  46576  fourierdlem51  46606  fourierdlem52  46607  fourierdlem63  46618  fourierdlem64  46619  fourierdlem65  46620  fourierdlem102  46657  fourierdlem114  46669  sge0f1o  46831  nnfoctbdjlem  46904  isomenndlem  46979  ovnsubaddlem1  47019  3f1oss1  47538  f1oresf1o2  47754  grimuhgr  48378  grimcnv  48379  isuspgrimlem  48386  grimedg  48426  isubgr3stgrlem8  48464  tposres3  49371  uptrlem1  49700  lmdran  50161  cmdlan  50162