Theorem f1ofo 6707

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

Syntax hints:   → wi 4  ^◡ccnv 5579  Fun wfun 6412  –onto→wfo 6416  –1-1-onto→wf1o 6417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425

This theorem is referenced by:  f1imacnv  6716  resin  6721  f1ococnv2  6726  fo00  6735  isoini  7189  isofrlem  7191  isoselem  7192  ncanth  7210  f1opw2  7502  f1dmex  7773  f1ovv  7774  f1oweALT  7788  wemoiso2  7790  curry1  7915  curry2  7918  smoiso2  8171  f1osetex  8605  bren  8701  brenOLD  8702  f1oeng  8714  en1  8765  en1OLD  8766  canth2  8866  domss2  8872  mapen  8877  ssenen  8887  phplem4  8895  php3  8899  dif1enlem  8905  ssfiALT  8919  domunfican  9017  fiint  9021  f1fi  9036  f1opwfi  9053  mapfien  9097  supisolem  9162  ordiso2  9204  ordtypelem10  9216  oismo  9229  wdomref  9261  brwdom2  9262  unxpwdom2  9277  cantnflt2  9361  cantnfp1lem3  9368  wemapwe  9385  infxpenc2lem1  9706  fseqen  9714  infpwfien  9749  infmap2  9905  ackbij2  9930  cff1  9945  cofsmo  9956  infpssr  9995  enfin2i  10008  fin23lem27  10015  enfin1ai  10071  fin1a2lem7  10093  axcclem  10144  ttukeylem1  10196  fpwwe2lem5  10322  fpwwe2lem8  10325  canthp1lem2  10340  tskuni  10470  gruen  10499  cnexALT  12655  fiinfnf1o  13992  hasheqf1oi  13994  hashfacen  14094  hashfacenOLD  14095  fsumf1o  15363  fsumss  15365  fprodf1o  15584  fprodss  15586  ruc  15880  unbenlem  16537  xpsfrn  17196  xpsbas  17200  xpsadd  17202  xpsmul  17203  xpssca  17204  xpsvsca  17205  xpsless  17206  xpsle  17207  imasmndf1  18339  sursubmefmnd  18450  imasgrpf1  18607  gicsubgen  18809  symgmov2  18910  symgextfo  18945  symgfixelsi  18958  giccyg  19416  gsumzres  19425  gsumzcl2  19426  gsumzf1o  19428  gsumzaddlem  19437  gsumconst  19450  gsumzmhm  19453  gsumzoppg  19460  dprdf1o  19550  gsumfsum  20577  znleval  20674  lmimlbs  20953  lbslcic  20958  coe1mul2lem2  21349  cmpfi  22467  idqtop  22765  basqtop  22770  tgqtop  22771  hmeontr  22828  hmeoimaf1o  22829  hmeoqtop  22834  cmphmph  22847  connhmph  22848  nrmhmph  22853  indishmph  22857  cmphaushmeo  22859  xpstps  22869  xpstopnlem2  22870  fmid  23019  tsmsf1o  23204  imasdsf1olem  23434  imasf1oxmet  23436  imasf1omet  23437  xpsdsfn  23438  imasf1oxms  23551  imasf1oms  23552  iccpnfhmeo  24014  cnheiborlem  24023  ovolctb  24559  ovolicc2lem4  24589  dyadmbl  24669  mbfimaopnlem  24724  itg1addlem4  24768  itg1addlem4OLD  24769  dvcnvrelem2  25087  dvcnvre  25088  deg1ldg  25162  deg1leb  25165  efifo  25608  logrn  25619  dvrelog  25697  efopnlem2  25717  fsumdvdsmul  26249  f1otrg  27136  axcontlem10  27244  edgusgrnbfin  27643  eupthvdres  28500  cnvunop  30181  counop  30184  idunop  30241  elunop2  30276  fmptco1f1o  30869  padct  30956  symgcom  31254  cycpmconjvlem  31310  cycpmconjslem2  31324  xrge0iifiso  31787  volmeas  32099  ballotlemro  32389  derangenlem  33033  subfacp1lem3  33044  subfacp1lem5  33046  erdsze2lem1  33065  cvmsss2  33136  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem9  35713  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem29  35733  poimirlem31  35735  mblfinlem2  35742  ismtybndlem  35891  ismtyres  35893  diaintclN  38999  dibintclN  39108  mapdrn  39590  dnnumch2  40786  kelac1  40804  lnmlmic  40829  pwslnmlem1  40833  pwfi2f1o  40837  gicabl  40840  imasgim  40841  isnumbasgrplem1  40842  ntrneifv2  41579  stoweidlem27  43458  fourierdlem20  43558  fourierdlem51  43588  fourierdlem52  43589  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem102  43639  fourierdlem114  43651  sge0f1o  43810  nnfoctbdjlem  43883  isomenndlem  43958  ovnsubaddlem1  43998  f1oresf1o2  44670  isomuspgrlem2d  45171