Theorem f1ofo 6832

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

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 5662  Fun wfun 6534  –onto→wfo 6538  –1-1-onto→wf1o 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-cleq 2757  df-ss 3923  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547

This theorem is used by:  f1imacnv  6841  resin  6847  f1ococnv2  6852  fo00  6861  f1ounsn  7279  f1ocoima  7310  isoini  7345  isofrlem  7347  isoselem  7348  ncanth  7374  f1opw2  7675  f1dmex  7960  f1ovv  7961  f1oweALT  7975  wemoiso2  7977  mptcnfimad  7989  curry1  8105  curry2  8108  smoiso2  8362  f1osetex  8862  bren  8959  f1oeng  8973  en1  9027  canth2  9125  domss2  9131  mapen  9136  ssenen  9146  dif1enlem  9151  ssfiALT  9165  phplem2  9196  php3  9200  f1fi  9281  domunfican  9288  fiint  9293  f1opwfi  9320  mapfien  9375  supisolem  9441  ordiso2  9484  ordtypelem10  9496  oismo  9509  wdomref  9541  brwdom2  9542  unxpwdom2  9557  cantnflt2  9649  cantnfp1lem3  9656  wemapwe  9673  infxpenc2lem1  10019  fseqen  10027  infpwfien  10062  infmap2  10216  ackbij2  10241  cff1  10257  cofsmo  10268  infpssr  10307  enfin2i  10320  fin23lem27  10327  enfin1ai  10383  fin1a2lem7  10405  axcclem  10456  ttukeylem1  10508  fpwwe2lem5  10637  fpwwe2lem8  10640  canthp1lem2  10655  tskuni  10785  gruen  10814  cnexALT  13028  fiinfnf1o  14406  hasheqf1oi  14407  hashfacen  14511  fsumf1o  15799  fsumss  15801  fprodf1o  16025  fprodss  16027  ruc  16323  unbenlem  16992  xpsfrn  17646  xpsbas  17650  xpsadd  17652  xpsmul  17653  xpssca  17654  xpsvsca  17655  xpsless  17656  xpsle  17657  imasmndf1  18873  sursubmefmnd  18994  imasgrpf1  19169  gicsubgen  19395  symgmov2  19504  symgextfo  19538  symgfixelsi  19551  giccyg  20016  gsumzres  20025  gsumzcl2  20026  gsumzf1o  20028  gsumzaddlem  20037  gsumconst  20050  gsumzmhm  20053  gsumzoppg  20060  dprdf1o  20150  imasrngf1  20302  imasringf1  20461  gsumfsum  21636  znleval  21756  lmimlbs  22038  lbslcic  22043  coe1mul2lem2  22481  cmpfi  23617  idqtop  23916  basqtop  23921  tgqtop  23922  hmeontr  23979  hmeoimaf1o  23980  hmeoqtop  23985  cmphmph  23998  connhmph  23999  nrmhmph  24004  indishmph  24008  cmphaushmeo  24010  xpstps  24020  xpstopnlem2  24021  fmid  24170  tsmsf1o  24355  imasdsf1olem  24583  imasf1oxmet  24585  imasf1omet  24586  xpsdsfn  24587  imasf1oxms  24699  imasf1oms  24700  iccpnfhmeo  25157  cnheiborlem  25166  ovolctb  25702  ovolicc2lem4  25732  dyadmbl  25812  mbfimaopnlem  25867  itg1addlem4  25911  dvcnvrelem2  26230  dvcnvre  26231  deg1ldg  26302  deg1leb  26305  efifo  26765  logrn  26776  dvrelog  26855  efopnlem2  26875  fsumdvdsmul  27412  f1otrg  29277  axcontlem10  29380  edgusgrnbfin  29783  eupthvdres  30659  cnvunop  32343  counop  32346  idunop  32403  elunop2  32438  fmptco1f1o  33051  padct  33135  mndlactf1o  33416  mndractf1o  33417  symgcom  33469  cycpmconjvlem  33527  cycpmconjslem2  33541  1arithidomlem2  33892  esplysply  34027  xrge0iifiso  34391  volmeas  34688  ballotlemro  34980  vonf1oonfo  35658  derangenlem  35702  subfacp1lem3  35713  subfacp1lem5  35715  erdsze2lem1  35734  cvmsss2  35805  poimirlem1  38331  poimirlem2  38332  poimirlem3  38333  poimirlem4  38334  poimirlem5  38335  poimirlem6  38336  poimirlem7  38337  poimirlem9  38339  poimirlem10  38340  poimirlem11  38341  poimirlem12  38342  poimirlem14  38344  poimirlem15  38345  poimirlem16  38346  poimirlem17  38347  poimirlem19  38349  poimirlem20  38350  poimirlem22  38352  poimirlem23  38353  poimirlem24  38354  poimirlem25  38355  poimirlem29  38359  poimirlem31  38361  mblfinlem2  38368  ismtybndlem  38517  ismtyres  38519  diaintclN  41892  dibintclN  42001  mapdrn  42483  aks6d1c1p5  42939  riccrng1  43349  ricdrng1  43356  dnnumch2  43832  kelac1  43850  lnmlmic  43875  pwslnmlem1  43879  pwfi2f1o  43883  gicabl  43886  imasgim  43887  isnumbasgrplem1  43888  ntrneifv2  44866  stoweidlem27  46801  fourierdlem20  46901  fourierdlem51  46931  fourierdlem52  46932  fourierdlem63  46943  fourierdlem64  46944  fourierdlem65  46945  fourierdlem102  46982  fourierdlem114  46994  sge0f1o  47156  nnfoctbdjlem  47229  isomenndlem  47304  ovnsubaddlem1  47344  3f1oss1  47872  f1oresf1o2  48088  grimuhgr  48712  grimcnv  48713  isuspgrimlem  48720  grimedg  48760  isubgr3stgrlem8  48798  tposres3  49718  uptrlem1  50047  lmdran  50508  cmdlan  50509