Theorem f1ofo 6770

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

Syntax hints:   → wi 4  ^◡ccnv 5613  Fun wfun 6475  –onto→wfo 6479  –1-1-onto→wf1o 6480

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 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-cleq 2723  df-ss 3914  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488

This theorem is referenced by:  f1imacnv  6779  resin  6785  f1ococnv2  6790  fo00  6799  f1ounsn  7206  f1ocoima  7237  isoini  7272  isofrlem  7274  isoselem  7275  ncanth  7301  f1opw2  7601  f1dmex  7889  f1ovv  7890  f1oweALT  7904  wemoiso2  7906  mptcnfimad  7918  curry1  8034  curry2  8037  smoiso2  8289  f1osetex  8783  bren  8879  f1oeng  8893  en1  8946  canth2  9043  domss2  9049  mapen  9054  ssenen  9064  dif1enlem  9069  ssfiALT  9083  phplem2  9114  php3  9118  f1fi  9198  domunfican  9206  fiint  9211  f1opwfi  9240  mapfien  9292  supisolem  9358  ordiso2  9401  ordtypelem10  9413  oismo  9426  wdomref  9458  brwdom2  9459  unxpwdom2  9474  cantnflt2  9563  cantnfp1lem3  9570  wemapwe  9587  infxpenc2lem1  9910  fseqen  9918  infpwfien  9953  infmap2  10108  ackbij2  10133  cff1  10149  cofsmo  10160  infpssr  10199  enfin2i  10212  fin23lem27  10219  enfin1ai  10275  fin1a2lem7  10297  axcclem  10348  ttukeylem1  10400  fpwwe2lem5  10526  fpwwe2lem8  10529  canthp1lem2  10544  tskuni  10674  gruen  10703  cnexALT  12884  fiinfnf1o  14257  hasheqf1oi  14258  hashfacen  14361  fsumf1o  15630  fsumss  15632  fprodf1o  15853  fprodss  15855  ruc  16152  unbenlem  16820  xpsfrn  17472  xpsbas  17476  xpsadd  17478  xpsmul  17479  xpssca  17480  xpsvsca  17481  xpsless  17482  xpsle  17483  imasmndf1  18684  sursubmefmnd  18804  imasgrpf1  18970  gicsubgen  19191  symgmov2  19300  symgextfo  19334  symgfixelsi  19347  giccyg  19812  gsumzres  19821  gsumzcl2  19822  gsumzf1o  19824  gsumzaddlem  19833  gsumconst  19846  gsumzmhm  19849  gsumzoppg  19856  dprdf1o  19946  imasrngf1  20096  imasringf1  20249  gsumfsum  21371  znleval  21491  lmimlbs  21773  lbslcic  21778  coe1mul2lem2  22182  cmpfi  23323  idqtop  23621  basqtop  23626  tgqtop  23627  hmeontr  23684  hmeoimaf1o  23685  hmeoqtop  23690  cmphmph  23703  connhmph  23704  nrmhmph  23709  indishmph  23713  cmphaushmeo  23715  xpstps  23725  xpstopnlem2  23726  fmid  23875  tsmsf1o  24060  imasdsf1olem  24288  imasf1oxmet  24290  imasf1omet  24291  xpsdsfn  24292  imasf1oxms  24404  imasf1oms  24405  iccpnfhmeo  24870  cnheiborlem  24880  ovolctb  25418  ovolicc2lem4  25448  dyadmbl  25528  mbfimaopnlem  25583  itg1addlem4  25627  dvcnvrelem2  25950  dvcnvre  25951  deg1ldg  26024  deg1leb  26027  efifo  26483  logrn  26494  dvrelog  26573  efopnlem2  26593  fsumdvdsmul  27132  fsumdvdsmulOLD  27134  f1otrg  28849  axcontlem10  28951  edgusgrnbfin  29351  eupthvdres  30215  cnvunop  31898  counop  31901  idunop  31958  elunop2  31993  fmptco1f1o  32615  padct  32701  mndlactf1o  33011  mndractf1o  33012  symgcom  33052  cycpmconjvlem  33110  cycpmconjslem2  33124  1arithidomlem2  33501  esplysply  33592  xrge0iifiso  33948  volmeas  34244  ballotlemro  34536  derangenlem  35215  subfacp1lem3  35226  subfacp1lem5  35228  erdsze2lem1  35247  cvmsss2  35318  poimirlem1  37671  poimirlem2  37672  poimirlem3  37673  poimirlem4  37674  poimirlem5  37675  poimirlem6  37676  poimirlem7  37677  poimirlem9  37679  poimirlem10  37680  poimirlem11  37681  poimirlem12  37682  poimirlem14  37684  poimirlem15  37685  poimirlem16  37686  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem22  37692  poimirlem23  37693  poimirlem24  37694  poimirlem25  37695  poimirlem29  37699  poimirlem31  37701  mblfinlem2  37708  ismtybndlem  37856  ismtyres  37858  diaintclN  41167  dibintclN  41276  mapdrn  41758  aks6d1c1p5  42215  riccrng1  42624  ricdrng1  42631  dnnumch2  43148  kelac1  43166  lnmlmic  43191  pwslnmlem1  43195  pwfi2f1o  43199  gicabl  43202  imasgim  43203  isnumbasgrplem1  43204  ntrneifv2  44183  stoweidlem27  46135  fourierdlem20  46235  fourierdlem51  46265  fourierdlem52  46266  fourierdlem63  46277  fourierdlem64  46278  fourierdlem65  46279  fourierdlem102  46316  fourierdlem114  46328  sge0f1o  46490  nnfoctbdjlem  46563  isomenndlem  46638  ovnsubaddlem1  46678  3f1oss1  47185  f1oresf1o2  47401  grimuhgr  47997  grimcnv  47998  isuspgrimlem  48005  grimedg  48045  isubgr3stgrlem8  48083  tposres3  48991  uptrlem1  49321  lmdran  49782  cmdlan  49783