Theorem f1ofo 6841

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

Syntax hints:   → wi 4  ^◡ccnv 5676  Fun wfun 6538  –onto→wfo 6542  –1-1-onto→wf1o 6543

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1087  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3956  df-ss 3966  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551

This theorem is referenced by:  f1imacnv  6850  resin  6856  f1ococnv2  6861  fo00  6870  isoini  7339  isofrlem  7341  isoselem  7342  ncanth  7367  f1opw2  7665  f1dmex  7947  f1ovv  7948  f1oweALT  7963  wemoiso2  7965  curry1  8094  curry2  8097  smoiso2  8373  f1osetex  8857  bren  8953  brenOLD  8954  f1oeng  8971  en1  9025  en1OLD  9026  canth2  9134  domss2  9140  mapen  9145  ssenen  9155  dif1enlem  9160  dif1enlemOLD  9161  ssfiALT  9178  phplem2  9212  php3  9216  phplem4OLD  9224  php3OLD  9228  domunfican  9324  fiint  9328  f1fi  9343  f1opwfi  9360  mapfien  9407  supisolem  9472  ordiso2  9514  ordtypelem10  9526  oismo  9539  wdomref  9571  brwdom2  9572  unxpwdom2  9587  cantnflt2  9672  cantnfp1lem3  9679  wemapwe  9696  infxpenc2lem1  10018  fseqen  10026  infpwfien  10061  infmap2  10217  ackbij2  10242  cff1  10257  cofsmo  10268  infpssr  10307  enfin2i  10320  fin23lem27  10327  enfin1ai  10383  fin1a2lem7  10405  axcclem  10456  ttukeylem1  10508  fpwwe2lem5  10634  fpwwe2lem8  10637  canthp1lem2  10652  tskuni  10782  gruen  10811  cnexALT  12976  fiinfnf1o  14316  hasheqf1oi  14317  hashfacen  14419  hashfacenOLD  14420  fsumf1o  15675  fsumss  15677  fprodf1o  15896  fprodss  15898  ruc  16192  unbenlem  16847  xpsfrn  17520  xpsbas  17524  xpsadd  17526  xpsmul  17527  xpssca  17528  xpsvsca  17529  xpsless  17530  xpsle  17531  imasmndf1  18700  sursubmefmnd  18815  imasgrpf1  18978  gicsubgen  19195  symgmov2  19298  symgextfo  19333  symgfixelsi  19346  giccyg  19811  gsumzres  19820  gsumzcl2  19821  gsumzf1o  19823  gsumzaddlem  19832  gsumconst  19845  gsumzmhm  19848  gsumzoppg  19855  dprdf1o  19945  imasrngf1  20074  imasringf1  20221  gsumfsum  21214  znleval  21331  lmimlbs  21612  lbslcic  21617  coe1mul2lem2  22012  cmpfi  23134  idqtop  23432  basqtop  23437  tgqtop  23438  hmeontr  23495  hmeoimaf1o  23496  hmeoqtop  23501  cmphmph  23514  connhmph  23515  nrmhmph  23520  indishmph  23524  cmphaushmeo  23526  xpstps  23536  xpstopnlem2  23537  fmid  23686  tsmsf1o  23871  imasdsf1olem  24101  imasf1oxmet  24103  imasf1omet  24104  xpsdsfn  24105  imasf1oxms  24220  imasf1oms  24221  iccpnfhmeo  24692  cnheiborlem  24702  ovolctb  25241  ovolicc2lem4  25271  dyadmbl  25351  mbfimaopnlem  25406  itg1addlem4  25450  itg1addlem4OLD  25451  dvcnvrelem2  25769  dvcnvre  25770  deg1ldg  25844  deg1leb  25847  efifo  26290  logrn  26301  dvrelog  26379  efopnlem2  26399  fsumdvdsmul  26933  f1otrg  28387  axcontlem10  28496  edgusgrnbfin  28895  eupthvdres  29753  cnvunop  31436  counop  31439  idunop  31496  elunop2  31531  fmptco1f1o  32122  padct  32209  symgcom  32512  cycpmconjvlem  32568  cycpmconjslem2  32582  xrge0iifiso  33211  volmeas  33525  ballotlemro  33817  derangenlem  34458  subfacp1lem3  34469  subfacp1lem5  34471  erdsze2lem1  34490  cvmsss2  34561  poimirlem1  36794  poimirlem2  36795  poimirlem3  36796  poimirlem4  36797  poimirlem5  36798  poimirlem6  36799  poimirlem7  36800  poimirlem9  36802  poimirlem10  36803  poimirlem11  36804  poimirlem12  36805  poimirlem14  36807  poimirlem15  36808  poimirlem16  36809  poimirlem17  36810  poimirlem19  36812  poimirlem20  36813  poimirlem22  36815  poimirlem23  36816  poimirlem24  36817  poimirlem25  36818  poimirlem29  36822  poimirlem31  36824  mblfinlem2  36831  ismtybndlem  36979  ismtyres  36981  diaintclN  40234  dibintclN  40343  mapdrn  40825  riccrng1  41402  ricdrng1  41408  dnnumch2  42091  kelac1  42109  lnmlmic  42134  pwslnmlem1  42138  pwfi2f1o  42142  gicabl  42145  imasgim  42146  isnumbasgrplem1  42147  ntrneifv2  43135  stoweidlem27  45043  fourierdlem20  45143  fourierdlem51  45173  fourierdlem52  45174  fourierdlem63  45185  fourierdlem64  45186  fourierdlem65  45187  fourierdlem102  45224  fourierdlem114  45236  sge0f1o  45398  nnfoctbdjlem  45471  isomenndlem  45546  ovnsubaddlem1  45586  f1oresf1o2  46299  isomuspgrlem2d  46799