Theorem f1ofo 6839

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

Syntax hints:   → wi 4  ^◡ccnv 5671  Fun wfun 6537  –onto→wfo 6541  –1-1-onto→wf1o 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-ex 1775  df-cleq 2718  df-ss 3963  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550

This theorem is referenced by:  f1imacnv  6848  resin  6854  f1ococnv2  6859  fo00  6868  isoini  7339  isofrlem  7341  isoselem  7342  ncanth  7367  f1opw2  7670  f1dmex  7959  f1ovv  7960  f1oweALT  7975  wemoiso2  7977  mptcnfimad  7989  curry1  8107  curry2  8110  smoiso2  8388  f1osetex  8877  bren  8973  brenOLD  8974  f1oeng  8991  en1  9046  en1OLD  9047  canth2  9157  domss2  9163  mapen  9168  ssenen  9178  dif1enlem  9183  dif1enlemOLD  9184  ssfiALT  9202  phplem2  9232  php3  9236  phplem4OLD  9244  php3OLD  9248  f1fi  9344  domunfican  9353  fiint  9358  fiintOLD  9359  f1opwfi  9390  mapfien  9441  supisolem  9506  ordiso2  9548  ordtypelem10  9560  oismo  9573  wdomref  9605  brwdom2  9606  unxpwdom2  9621  cantnflt2  9706  cantnfp1lem3  9713  wemapwe  9730  infxpenc2lem1  10052  fseqen  10060  infpwfien  10095  infmap2  10249  ackbij2  10274  cff1  10289  cofsmo  10300  infpssr  10339  enfin2i  10352  fin23lem27  10359  enfin1ai  10415  fin1a2lem7  10437  axcclem  10488  ttukeylem1  10540  fpwwe2lem5  10666  fpwwe2lem8  10669  canthp1lem2  10684  tskuni  10814  gruen  10843  cnexALT  13013  fiinfnf1o  14359  hasheqf1oi  14360  hashfacen  14463  hashfacenOLD  14464  fsumf1o  15719  fsumss  15721  fprodf1o  15940  fprodss  15942  ruc  16237  unbenlem  16902  xpsfrn  17575  xpsbas  17579  xpsadd  17581  xpsmul  17582  xpssca  17583  xpsvsca  17584  xpsless  17585  xpsle  17586  imasmndf1  18758  sursubmefmnd  18878  imasgrpf1  19044  gicsubgen  19266  symgmov2  19378  symgextfo  19413  symgfixelsi  19426  giccyg  19891  gsumzres  19900  gsumzcl2  19901  gsumzf1o  19903  gsumzaddlem  19912  gsumconst  19925  gsumzmhm  19928  gsumzoppg  19935  dprdf1o  20025  imasrngf1  20154  imasringf1  20303  gsumfsum  21424  znleval  21545  lmimlbs  21827  lbslcic  21832  coe1mul2lem2  22252  cmpfi  23397  idqtop  23695  basqtop  23700  tgqtop  23701  hmeontr  23758  hmeoimaf1o  23759  hmeoqtop  23764  cmphmph  23777  connhmph  23778  nrmhmph  23783  indishmph  23787  cmphaushmeo  23789  xpstps  23799  xpstopnlem2  23800  fmid  23949  tsmsf1o  24134  imasdsf1olem  24364  imasf1oxmet  24366  imasf1omet  24367  xpsdsfn  24368  imasf1oxms  24483  imasf1oms  24484  iccpnfhmeo  24955  cnheiborlem  24965  ovolctb  25504  ovolicc2lem4  25534  dyadmbl  25614  mbfimaopnlem  25669  itg1addlem4  25713  itg1addlem4OLD  25714  dvcnvrelem2  26036  dvcnvre  26037  deg1ldg  26113  deg1leb  26116  efifo  26568  logrn  26579  dvrelog  26658  efopnlem2  26678  fsumdvdsmul  27217  fsumdvdsmulOLD  27219  f1otrg  28792  axcontlem10  28901  edgusgrnbfin  29303  eupthvdres  30162  cnvunop  31845  counop  31848  idunop  31905  elunop2  31940  fmptco1f1o  32547  padct  32630  symgcom  32962  cycpmconjvlem  33020  cycpmconjslem2  33034  1arithidomlem2  33414  xrge0iifiso  33760  volmeas  34074  ballotlemro  34366  derangenlem  35009  subfacp1lem3  35020  subfacp1lem5  35022  erdsze2lem1  35041  cvmsss2  35112  poimirlem1  37332  poimirlem2  37333  poimirlem3  37334  poimirlem4  37335  poimirlem5  37336  poimirlem6  37337  poimirlem7  37338  poimirlem9  37340  poimirlem10  37341  poimirlem11  37342  poimirlem12  37343  poimirlem14  37345  poimirlem15  37346  poimirlem16  37347  poimirlem17  37348  poimirlem19  37350  poimirlem20  37351  poimirlem22  37353  poimirlem23  37354  poimirlem24  37355  poimirlem25  37356  poimirlem29  37360  poimirlem31  37362  mblfinlem2  37369  ismtybndlem  37517  ismtyres  37519  diaintclN  40767  dibintclN  40876  mapdrn  41358  aks6d1c1p5  41821  riccrng1  42208  ricdrng1  42215  dnnumch2  42740  kelac1  42758  lnmlmic  42783  pwslnmlem1  42787  pwfi2f1o  42791  gicabl  42794  imasgim  42795  isnumbasgrplem1  42796  ntrneifv2  43781  stoweidlem27  45681  fourierdlem20  45781  fourierdlem51  45811  fourierdlem52  45812  fourierdlem63  45823  fourierdlem64  45824  fourierdlem65  45825  fourierdlem102  45862  fourierdlem114  45874  sge0f1o  46036  nnfoctbdjlem  46109  isomenndlem  46184  ovnsubaddlem1  46224  f1oresf1o2  46937  uspgrimprop  47485  isuspgrimlem  47486  grimuhgr  47490  grimcnv  47491