Theorem f1ofo 6774

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

Syntax hints:   → wi 4  ^◡ccnv 5617  Fun wfun 6479  –onto→wfo 6483  –1-1-onto→wf1o 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-ex 1787  df-cleq 2731  df-ss 3900  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492

This theorem is referenced by:  f1imacnv  6783  resin  6789  f1ococnv2  6794  fo00  6803  f1ounsn  7216  f1ocoima  7247  isoini  7282  isofrlem  7284  isoselem  7285  ncanth  7311  f1opw2  7611  f1dmex  7899  f1ovv  7900  f1oweALT  7914  wemoiso2  7916  mptcnfimad  7928  curry1  8043  curry2  8046  smoiso2  8299  f1osetex  8796  bren  8893  f1oeng  8907  en1  8961  canth2  9058  domss2  9064  mapen  9069  ssenen  9079  dif1enlem  9084  ssfiALT  9098  phplem2  9129  php3  9133  f1fi  9214  domunfican  9222  fiint  9227  f1opwfi  9256  mapfien  9311  supisolem  9377  ordiso2  9420  ordtypelem10  9432  oismo  9445  wdomref  9477  brwdom2  9478  unxpwdom2  9493  cantnflt2  9585  cantnfp1lem3  9592  wemapwe  9609  infxpenc2lem1  9932  fseqen  9940  infpwfien  9975  infmap2  10130  ackbij2  10155  cff1  10171  cofsmo  10182  infpssr  10221  enfin2i  10234  fin23lem27  10241  enfin1ai  10297  fin1a2lem7  10319  axcclem  10370  ttukeylem1  10422  fpwwe2lem5  10549  fpwwe2lem8  10552  canthp1lem2  10567  tskuni  10697  gruen  10726  cnexALT  12927  fiinfnf1o  14303  hasheqf1oi  14304  hashfacen  14407  fsumf1o  15676  fsumss  15678  fprodf1o  15902  fprodss  15904  ruc  16201  unbenlem  16870  xpsfrn  17523  xpsbas  17527  xpsadd  17529  xpsmul  17530  xpssca  17531  xpsvsca  17532  xpsless  17533  xpsle  17534  imasmndf1  18735  sursubmefmnd  18855  imasgrpf1  19024  gicsubgen  19245  symgmov2  19354  symgextfo  19388  symgfixelsi  19401  giccyg  19866  gsumzres  19875  gsumzcl2  19876  gsumzf1o  19878  gsumzaddlem  19887  gsumconst  19900  gsumzmhm  19903  gsumzoppg  19910  dprdf1o  20000  imasrngf1  20150  imasringf1  20302  gsumfsum  21409  znleval  21529  lmimlbs  21811  lbslcic  21816  coe1mul2lem2  22254  cmpfi  23391  idqtop  23689  basqtop  23694  tgqtop  23695  hmeontr  23752  hmeoimaf1o  23753  hmeoqtop  23758  cmphmph  23771  connhmph  23772  nrmhmph  23777  indishmph  23781  cmphaushmeo  23783  xpstps  23793  xpstopnlem2  23794  fmid  23943  tsmsf1o  24128  imasdsf1olem  24356  imasf1oxmet  24358  imasf1omet  24359  xpsdsfn  24360  imasf1oxms  24472  imasf1oms  24473  iccpnfhmeo  24930  cnheiborlem  24939  ovolctb  25475  ovolicc2lem4  25505  dyadmbl  25585  mbfimaopnlem  25640  itg1addlem4  25684  dvcnvrelem2  26003  dvcnvre  26004  deg1ldg  26075  deg1leb  26078  efifo  26529  logrn  26540  dvrelog  26619  efopnlem2  26639  fsumdvdsmul  27176  f1otrg  28957  axcontlem10  29060  edgusgrnbfin  29460  eupthvdres  30323  cnvunop  32007  counop  32010  idunop  32067  elunop2  32102  fmptco1f1o  32725  padct  32810  mndlactf1o  33109  mndractf1o  33110  symgcom  33164  cycpmconjvlem  33222  cycpmconjslem2  33236  1arithidomlem2  33619  esplysply  33755  xrge0iifiso  34119  volmeas  34415  ballotlemro  34707  derangenlem  35399  subfacp1lem3  35410  subfacp1lem5  35412  erdsze2lem1  35431  cvmsss2  35502  poimirlem1  37988  poimirlem2  37989  poimirlem3  37990  poimirlem4  37991  poimirlem5  37992  poimirlem6  37993  poimirlem7  37994  poimirlem9  37996  poimirlem10  37997  poimirlem11  37998  poimirlem12  37999  poimirlem14  38001  poimirlem15  38002  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem22  38009  poimirlem23  38010  poimirlem24  38011  poimirlem25  38012  poimirlem29  38016  poimirlem31  38018  mblfinlem2  38025  ismtybndlem  38173  ismtyres  38175  diaintclN  41550  dibintclN  41659  mapdrn  42141  aks6d1c1p5  42597  riccrng1  43007  ricdrng1  43014  dnnumch2  43490  kelac1  43508  lnmlmic  43533  pwslnmlem1  43537  pwfi2f1o  43541  gicabl  43544  imasgim  43545  isnumbasgrplem1  43546  ntrneifv2  44524  stoweidlem27  46470  fourierdlem20  46570  fourierdlem51  46600  fourierdlem52  46601  fourierdlem63  46612  fourierdlem64  46613  fourierdlem65  46614  fourierdlem102  46651  fourierdlem114  46663  sge0f1o  46825  nnfoctbdjlem  46898  isomenndlem  46973  ovnsubaddlem1  47013  3f1oss1  47538  f1oresf1o2  47754  grimuhgr  48378  grimcnv  48379  isuspgrimlem  48386  grimedg  48426  isubgr3stgrlem8  48464  tposres3  49371  uptrlem1  49700  lmdran  50161  cmdlan  50162