Theorem f1ofo 6814

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

Syntax hints:   → wi 4  ^◡ccnv 5646  Fun wfun 6515  –onto→wfo 6519  –1-1-onto→wf1o 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1100  df-ex 1800  df-cleq 2754  df-ss 3921  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528

This theorem is referenced by:  f1imacnv  6823  resin  6829  f1ococnv2  6834  fo00  6843  f1ounsn  7256  f1ocoima  7287  isoini  7322  isofrlem  7324  isoselem  7325  ncanth  7351  f1opw2  7651  f1dmex  7938  f1ovv  7939  f1oweALT  7953  wemoiso2  7955  mptcnfimad  7967  curry1  8083  curry2  8086  smoiso2  8340  f1osetex  8840  bren  8937  f1oeng  8951  en1  9005  canth2  9102  domss2  9108  mapen  9113  ssenen  9123  dif1enlem  9128  ssfiALT  9142  phplem2  9173  php3  9177  f1fi  9258  domunfican  9266  fiint  9271  f1opwfi  9299  mapfien  9354  supisolem  9420  ordiso2  9463  ordtypelem10  9475  oismo  9488  wdomref  9520  brwdom2  9521  unxpwdom2  9536  cantnflt2  9628  cantnfp1lem3  9635  wemapwe  9652  infxpenc2lem1  9975  fseqen  9983  infpwfien  10018  infmap2  10173  ackbij2  10198  cff1  10215  cofsmo  10226  infpssr  10265  enfin2i  10278  fin23lem27  10285  enfin1ai  10341  fin1a2lem7  10363  axcclem  10414  ttukeylem1  10466  fpwwe2lem5  10593  fpwwe2lem8  10596  canthp1lem2  10611  tskuni  10741  gruen  10770  cnexALT  12987  fiinfnf1o  14363  hasheqf1oi  14364  hashfacen  14467  fsumf1o  15750  fsumss  15752  fprodf1o  15976  fprodss  15978  ruc  16275  unbenlem  16944  xpsfrn  17598  xpsbas  17602  xpsadd  17604  xpsmul  17605  xpssca  17606  xpsvsca  17607  xpsless  17608  xpsle  17609  imasmndf1  18810  sursubmefmnd  18930  imasgrpf1  19099  gicsubgen  19319  symgmov2  19428  symgextfo  19462  symgfixelsi  19475  giccyg  19940  gsumzres  19949  gsumzcl2  19950  gsumzf1o  19952  gsumzaddlem  19961  gsumconst  19974  gsumzmhm  19977  gsumzoppg  19984  dprdf1o  20074  imasrngf1  20224  imasringf1  20380  gsumfsum  21486  znleval  21606  lmimlbs  21888  lbslcic  21893  coe1mul2lem2  22331  cmpfi  23468  idqtop  23766  basqtop  23771  tgqtop  23772  hmeontr  23829  hmeoimaf1o  23830  hmeoqtop  23835  cmphmph  23848  connhmph  23849  nrmhmph  23854  indishmph  23858  cmphaushmeo  23860  xpstps  23870  xpstopnlem2  23871  fmid  24020  tsmsf1o  24205  imasdsf1olem  24433  imasf1oxmet  24435  imasf1omet  24436  xpsdsfn  24437  imasf1oxms  24549  imasf1oms  24550  iccpnfhmeo  25007  cnheiborlem  25016  ovolctb  25552  ovolicc2lem4  25582  dyadmbl  25662  mbfimaopnlem  25717  itg1addlem4  25761  dvcnvrelem2  26080  dvcnvre  26081  deg1ldg  26152  deg1leb  26155  efifo  26612  logrn  26623  dvrelog  26702  efopnlem2  26722  fsumdvdsmul  27259  f1otrg  29071  axcontlem10  29174  edgusgrnbfin  29574  eupthvdres  30437  cnvunop  32121  counop  32124  idunop  32181  elunop2  32216  fmptco1f1o  32835  padct  32920  mndlactf1o  33208  mndractf1o  33209  symgcom  33263  cycpmconjvlem  33321  cycpmconjslem2  33335  1arithidomlem2  33732  esplysply  33868  xrge0iifiso  34232  volmeas  34528  ballotlemro  34820  vonf1oonfo  35458  derangenlem  35521  subfacp1lem3  35532  subfacp1lem5  35534  erdsze2lem1  35553  cvmsss2  35624  poimirlem1  38120  poimirlem2  38121  poimirlem3  38122  poimirlem4  38123  poimirlem5  38124  poimirlem6  38125  poimirlem7  38126  poimirlem9  38128  poimirlem10  38129  poimirlem11  38130  poimirlem12  38131  poimirlem14  38133  poimirlem15  38134  poimirlem16  38135  poimirlem17  38136  poimirlem19  38138  poimirlem20  38139  poimirlem22  38141  poimirlem23  38142  poimirlem24  38143  poimirlem25  38144  poimirlem29  38148  poimirlem31  38150  mblfinlem2  38157  ismtybndlem  38305  ismtyres  38307  diaintclN  41682  dibintclN  41791  mapdrn  42273  aks6d1c1p5  42729  riccrng1  43139  ricdrng1  43146  dnnumch2  43622  kelac1  43640  lnmlmic  43665  pwslnmlem1  43669  pwfi2f1o  43673  gicabl  43676  imasgim  43677  isnumbasgrplem1  43678  ntrneifv2  44656  stoweidlem27  46601  fourierdlem20  46701  fourierdlem51  46731  fourierdlem52  46732  fourierdlem63  46743  fourierdlem64  46744  fourierdlem65  46745  fourierdlem102  46782  fourierdlem114  46794  sge0f1o  46956  nnfoctbdjlem  47029  isomenndlem  47104  ovnsubaddlem1  47144  3f1oss1  47669  f1oresf1o2  47885  grimuhgr  48509  grimcnv  48510  isuspgrimlem  48517  grimedg  48557  isubgr3stgrlem8  48595  tposres3  49502  uptrlem1  49831  lmdran  50292  cmdlan  50293