Theorem f1ofo 6597

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

Syntax hints:   → wi 4  ^◡ccnv 5518  Fun wfun 6318  –onto→wfo 6322  –1-1-onto→wf1o 6323

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331

This theorem is referenced by:  f1imacnv  6606  resin  6611  f1ococnv2  6616  fo00  6625  isoini  7070  isofrlem  7072  isoselem  7073  ncanth  7091  f1opw2  7380  f1dmex  7640  f1ovv  7641  f1oweALT  7655  wemoiso2  7657  curry1  7782  curry2  7785  smoiso2  7989  bren  8501  f1oeng  8511  en1  8559  canth2  8654  domss2  8660  mapen  8665  ssenen  8675  phplem4  8683  php3  8687  ssfi  8722  domunfican  8775  fiint  8779  f1fi  8795  f1opwfi  8812  mapfien  8855  supisolem  8921  ordiso2  8963  ordtypelem10  8975  oismo  8988  wdomref  9020  brwdom2  9021  unxpwdom2  9036  cantnflt2  9120  cantnfp1lem3  9127  wemapwe  9144  infxpenc2lem1  9430  fseqen  9438  infpwfien  9473  infmap2  9629  ackbij2  9654  cff1  9669  cofsmo  9680  infpssr  9719  enfin2i  9732  fin23lem27  9739  enfin1ai  9795  fin1a2lem7  9817  axcclem  9868  ttukeylem1  9920  fpwwe2lem6  10046  fpwwe2lem9  10049  canthp1lem2  10064  tskuni  10194  gruen  10223  cnexALT  12373  fiinfnf1o  13706  hasheqf1oi  13708  hashfacen  13808  fsumf1o  15072  fsumss  15074  fprodf1o  15292  fprodss  15294  ruc  15588  unbenlem  16234  xpsfrn  16833  xpsbas  16837  xpsadd  16839  xpsmul  16840  xpssca  16841  xpsvsca  16842  xpsless  16843  xpsle  16844  imasmndf1  17942  sursubmefmnd  18053  imasgrpf1  18208  gicsubgen  18410  symgmov2  18508  symgextfo  18542  symgfixelsi  18555  giccyg  19013  gsumzres  19022  gsumzcl2  19023  gsumzf1o  19025  gsumzaddlem  19034  gsumconst  19047  gsumzmhm  19050  gsumzoppg  19057  dprdf1o  19147  gsumfsum  20158  znleval  20246  lmimlbs  20525  lbslcic  20530  coe1mul2lem2  20897  cmpfi  22013  idqtop  22311  basqtop  22316  tgqtop  22317  hmeontr  22374  hmeoimaf1o  22375  hmeoqtop  22380  cmphmph  22393  connhmph  22394  nrmhmph  22399  indishmph  22403  cmphaushmeo  22405  xpstps  22415  xpstopnlem2  22416  fmid  22565  tsmsf1o  22750  imasdsf1olem  22980  imasf1oxmet  22982  imasf1omet  22983  xpsdsfn  22984  imasf1oxms  23096  imasf1oms  23097  iccpnfhmeo  23550  cnheiborlem  23559  ovolctb  24094  ovolicc2lem4  24124  dyadmbl  24204  mbfimaopnlem  24259  itg1addlem4  24303  dvcnvrelem2  24621  dvcnvre  24622  deg1ldg  24693  deg1leb  24696  efifo  25139  logrn  25150  dvrelog  25228  efopnlem2  25248  fsumdvdsmul  25780  f1otrg  26665  axcontlem10  26767  edgusgrnbfin  27163  eupthvdres  28020  cnvunop  29701  counop  29704  idunop  29761  elunop2  29796  fmptco1f1o  30392  padct  30481  symgcom  30777  cycpmconjvlem  30833  cycpmconjslem2  30847  xrge0iifiso  31288  volmeas  31600  ballotlemro  31890  derangenlem  32531  subfacp1lem3  32542  subfacp1lem5  32544  erdsze2lem1  32563  cvmsss2  32634  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem9  35066  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem14  35071  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem22  35079  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem29  35086  poimirlem31  35088  mblfinlem2  35095  ismtybndlem  35244  ismtyres  35246  diaintclN  38354  dibintclN  38463  mapdrn  38945  dnnumch2  39989  kelac1  40007  lnmlmic  40032  pwslnmlem1  40036  pwfi2f1o  40040  gicabl  40043  imasgim  40044  isnumbasgrplem1  40045  ntrneifv2  40783  stoweidlem27  42669  fourierdlem20  42769  fourierdlem51  42799  fourierdlem52  42800  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem102  42850  fourierdlem114  42862  sge0f1o  43021  nnfoctbdjlem  43094  isomenndlem  43169  ovnsubaddlem1  43209  f1oresf1o2  43847  isomuspgrlem2d  44349