Theorem f1ofo 6771

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

Syntax hints:   → wi 4  ^◡ccnv 5618  Fun wfun 6476  –onto→wfo 6480  –1-1-onto→wf1o 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-cleq 2721  df-ss 3920  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489

This theorem is referenced by:  f1imacnv  6780  resin  6786  f1ococnv2  6791  fo00  6800  f1ounsn  7209  f1ocoima  7240  isoini  7275  isofrlem  7277  isoselem  7278  ncanth  7304  f1opw2  7604  f1dmex  7892  f1ovv  7893  f1oweALT  7907  wemoiso2  7909  mptcnfimad  7921  curry1  8037  curry2  8040  smoiso2  8292  f1osetex  8786  bren  8882  f1oeng  8896  en1  8949  canth2  9047  domss2  9053  mapen  9058  ssenen  9068  dif1enlem  9073  ssfiALT  9088  phplem2  9119  php3  9123  f1fi  9203  domunfican  9211  fiint  9216  fiintOLD  9217  f1opwfi  9246  mapfien  9298  supisolem  9364  ordiso2  9407  ordtypelem10  9419  oismo  9432  wdomref  9464  brwdom2  9465  unxpwdom2  9480  cantnflt2  9569  cantnfp1lem3  9576  wemapwe  9593  infxpenc2lem1  9913  fseqen  9921  infpwfien  9956  infmap2  10111  ackbij2  10136  cff1  10152  cofsmo  10163  infpssr  10202  enfin2i  10215  fin23lem27  10222  enfin1ai  10278  fin1a2lem7  10300  axcclem  10351  ttukeylem1  10403  fpwwe2lem5  10529  fpwwe2lem8  10532  canthp1lem2  10547  tskuni  10677  gruen  10706  cnexALT  12887  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  18650  sursubmefmnd  18770  imasgrpf1  18936  gicsubgen  19158  symgmov2  19267  symgextfo  19301  symgfixelsi  19314  giccyg  19779  gsumzres  19788  gsumzcl2  19789  gsumzf1o  19791  gsumzaddlem  19800  gsumconst  19813  gsumzmhm  19816  gsumzoppg  19823  dprdf1o  19913  imasrngf1  20063  imasringf1  20216  gsumfsum  21341  znleval  21461  lmimlbs  21743  lbslcic  21748  coe1mul2lem2  22152  cmpfi  23293  idqtop  23591  basqtop  23596  tgqtop  23597  hmeontr  23654  hmeoimaf1o  23655  hmeoqtop  23660  cmphmph  23673  connhmph  23674  nrmhmph  23679  indishmph  23683  cmphaushmeo  23685  xpstps  23695  xpstopnlem2  23696  fmid  23845  tsmsf1o  24030  imasdsf1olem  24259  imasf1oxmet  24261  imasf1omet  24262  xpsdsfn  24263  imasf1oxms  24375  imasf1oms  24376  iccpnfhmeo  24841  cnheiborlem  24851  ovolctb  25389  ovolicc2lem4  25419  dyadmbl  25499  mbfimaopnlem  25554  itg1addlem4  25598  dvcnvrelem2  25921  dvcnvre  25922  deg1ldg  25995  deg1leb  25998  efifo  26454  logrn  26465  dvrelog  26544  efopnlem2  26564  fsumdvdsmul  27103  fsumdvdsmulOLD  27105  f1otrg  28816  axcontlem10  28918  edgusgrnbfin  29318  eupthvdres  30179  cnvunop  31862  counop  31865  idunop  31922  elunop2  31957  fmptco1f1o  32576  padct  32662  mndlactf1o  32984  mndractf1o  32985  symgcom  33025  cycpmconjvlem  33083  cycpmconjslem2  33097  1arithidomlem2  33473  xrge0iifiso  33902  volmeas  34198  ballotlemro  34491  derangenlem  35148  subfacp1lem3  35159  subfacp1lem5  35161  erdsze2lem1  35180  cvmsss2  35251  poimirlem1  37605  poimirlem2  37606  poimirlem3  37607  poimirlem4  37608  poimirlem5  37609  poimirlem6  37610  poimirlem7  37611  poimirlem9  37613  poimirlem10  37614  poimirlem11  37615  poimirlem12  37616  poimirlem14  37618  poimirlem15  37619  poimirlem16  37620  poimirlem17  37621  poimirlem19  37623  poimirlem20  37624  poimirlem22  37626  poimirlem23  37627  poimirlem24  37628  poimirlem25  37629  poimirlem29  37633  poimirlem31  37635  mblfinlem2  37642  ismtybndlem  37790  ismtyres  37792  diaintclN  41041  dibintclN  41150  mapdrn  41632  aks6d1c1p5  42089  riccrng1  42498  ricdrng1  42505  dnnumch2  43022  kelac1  43040  lnmlmic  43065  pwslnmlem1  43069  pwfi2f1o  43073  gicabl  43076  imasgim  43077  isnumbasgrplem1  43078  ntrneifv2  44057  stoweidlem27  46012  fourierdlem20  46112  fourierdlem51  46142  fourierdlem52  46143  fourierdlem63  46154  fourierdlem64  46155  fourierdlem65  46156  fourierdlem102  46193  fourierdlem114  46205  sge0f1o  46367  nnfoctbdjlem  46440  isomenndlem  46515  ovnsubaddlem1  46555  3f1oss1  47063  f1oresf1o2  47279  grimuhgr  47875  grimcnv  47876  isuspgrimlem  47883  grimedg  47923  isubgr3stgrlem8  47961  tposres3  48869  uptrlem1  49199  lmdran  49660  cmdlan  49661