Theorem f1ofo 6781

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

Syntax hints:   → wi 4  ^◡ccnv 5623  Fun wfun 6486  –onto→wfo 6490  –1-1-onto→wf1o 6491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-cleq 2728  df-ss 3918  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499

This theorem is referenced by:  f1imacnv  6790  resin  6796  f1ococnv2  6801  fo00  6810  f1ounsn  7218  f1ocoima  7249  isoini  7284  isofrlem  7286  isoselem  7287  ncanth  7313  f1opw2  7613  f1dmex  7901  f1ovv  7902  f1oweALT  7916  wemoiso2  7918  mptcnfimad  7930  curry1  8046  curry2  8049  smoiso2  8301  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  9582  cantnfp1lem3  9589  wemapwe  9606  infxpenc2lem1  9929  fseqen  9937  infpwfien  9972  infmap2  10127  ackbij2  10152  cff1  10168  cofsmo  10179  infpssr  10218  enfin2i  10231  fin23lem27  10238  enfin1ai  10294  fin1a2lem7  10316  axcclem  10367  ttukeylem1  10419  fpwwe2lem5  10546  fpwwe2lem8  10549  canthp1lem2  10564  tskuni  10694  gruen  10723  cnexALT  12899  fiinfnf1o  14273  hasheqf1oi  14274  hashfacen  14377  fsumf1o  15646  fsumss  15648  fprodf1o  15869  fprodss  15871  ruc  16168  unbenlem  16836  xpsfrn  17489  xpsbas  17493  xpsadd  17495  xpsmul  17496  xpssca  17497  xpsvsca  17498  xpsless  17499  xpsle  17500  imasmndf1  18701  sursubmefmnd  18821  imasgrpf1  18987  gicsubgen  19208  symgmov2  19317  symgextfo  19351  symgfixelsi  19364  giccyg  19829  gsumzres  19838  gsumzcl2  19839  gsumzf1o  19841  gsumzaddlem  19850  gsumconst  19863  gsumzmhm  19866  gsumzoppg  19873  dprdf1o  19963  imasrngf1  20113  imasringf1  20267  gsumfsum  21389  znleval  21509  lmimlbs  21791  lbslcic  21796  coe1mul2lem2  22210  cmpfi  23352  idqtop  23650  basqtop  23655  tgqtop  23656  hmeontr  23713  hmeoimaf1o  23714  hmeoqtop  23719  cmphmph  23732  connhmph  23733  nrmhmph  23738  indishmph  23742  cmphaushmeo  23744  xpstps  23754  xpstopnlem2  23755  fmid  23904  tsmsf1o  24089  imasdsf1olem  24317  imasf1oxmet  24319  imasf1omet  24320  xpsdsfn  24321  imasf1oxms  24433  imasf1oms  24434  iccpnfhmeo  24899  cnheiborlem  24909  ovolctb  25447  ovolicc2lem4  25477  dyadmbl  25557  mbfimaopnlem  25612  itg1addlem4  25656  dvcnvrelem2  25979  dvcnvre  25980  deg1ldg  26053  deg1leb  26056  efifo  26512  logrn  26523  dvrelog  26602  efopnlem2  26622  fsumdvdsmul  27161  fsumdvdsmulOLD  27163  f1otrg  28943  axcontlem10  29046  edgusgrnbfin  29446  eupthvdres  30310  cnvunop  31993  counop  31996  idunop  32053  elunop2  32088  fmptco1f1o  32711  padct  32797  mndlactf1o  33112  mndractf1o  33113  symgcom  33165  cycpmconjvlem  33223  cycpmconjslem2  33237  1arithidomlem2  33617  esplysply  33729  xrge0iifiso  34092  volmeas  34388  ballotlemro  34680  derangenlem  35365  subfacp1lem3  35376  subfacp1lem5  35378  erdsze2lem1  35397  cvmsss2  35468  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem9  37830  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem14  37835  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem22  37843  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem29  37850  poimirlem31  37852  mblfinlem2  37859  ismtybndlem  38007  ismtyres  38009  diaintclN  41328  dibintclN  41437  mapdrn  41919  aks6d1c1p5  42376  riccrng1  42786  ricdrng1  42793  dnnumch2  43297  kelac1  43315  lnmlmic  43340  pwslnmlem1  43344  pwfi2f1o  43348  gicabl  43351  imasgim  43352  isnumbasgrplem1  43353  ntrneifv2  44331  stoweidlem27  46281  fourierdlem20  46381  fourierdlem51  46411  fourierdlem52  46412  fourierdlem63  46423  fourierdlem64  46424  fourierdlem65  46425  fourierdlem102  46462  fourierdlem114  46474  sge0f1o  46636  nnfoctbdjlem  46709  isomenndlem  46784  ovnsubaddlem1  46824  3f1oss1  47331  f1oresf1o2  47547  grimuhgr  48143  grimcnv  48144  isuspgrimlem  48151  grimedg  48191  isubgr3stgrlem8  48229  tposres3  49136  uptrlem1  49465  lmdran  49926  cmdlan  49927