Theorem f1ofo 6721

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

Syntax hints:   → wi 4  ^◡ccnv 5589  Fun wfun 6426  –onto→wfo 6430  –1-1-onto→wf1o 6431

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439

This theorem is referenced by:  f1imacnv  6730  resin  6735  f1ococnv2  6740  fo00  6749  isoini  7205  isofrlem  7207  isoselem  7208  ncanth  7226  f1opw2  7518  f1dmex  7793  f1ovv  7794  f1oweALT  7808  wemoiso2  7810  curry1  7935  curry2  7938  smoiso2  8191  f1osetex  8630  bren  8726  brenOLD  8727  f1oeng  8742  en1  8794  en1OLD  8795  canth2  8899  domss2  8905  mapen  8910  ssenen  8920  dif1enlem  8925  ssfiALT  8939  phplem2  8972  php3  8976  phplem4OLD  8985  php3OLD  8989  domunfican  9065  fiint  9069  f1fi  9084  f1opwfi  9101  mapfien  9145  supisolem  9210  ordiso2  9252  ordtypelem10  9264  oismo  9277  wdomref  9309  brwdom2  9310  unxpwdom2  9325  cantnflt2  9409  cantnfp1lem3  9416  wemapwe  9433  infxpenc2lem1  9776  fseqen  9784  infpwfien  9819  infmap2  9975  ackbij2  10000  cff1  10015  cofsmo  10026  infpssr  10065  enfin2i  10078  fin23lem27  10085  enfin1ai  10141  fin1a2lem7  10163  axcclem  10214  ttukeylem1  10266  fpwwe2lem5  10392  fpwwe2lem8  10395  canthp1lem2  10410  tskuni  10540  gruen  10569  cnexALT  12725  fiinfnf1o  14062  hasheqf1oi  14064  hashfacen  14164  hashfacenOLD  14165  fsumf1o  15433  fsumss  15435  fprodf1o  15654  fprodss  15656  ruc  15950  unbenlem  16607  xpsfrn  17277  xpsbas  17281  xpsadd  17283  xpsmul  17284  xpssca  17285  xpsvsca  17286  xpsless  17287  xpsle  17288  imasmndf1  18422  sursubmefmnd  18533  imasgrpf1  18690  gicsubgen  18892  symgmov2  18993  symgextfo  19028  symgfixelsi  19041  giccyg  19499  gsumzres  19508  gsumzcl2  19509  gsumzf1o  19511  gsumzaddlem  19520  gsumconst  19533  gsumzmhm  19536  gsumzoppg  19543  dprdf1o  19633  gsumfsum  20663  znleval  20760  lmimlbs  21041  lbslcic  21046  coe1mul2lem2  21437  cmpfi  22557  idqtop  22855  basqtop  22860  tgqtop  22861  hmeontr  22918  hmeoimaf1o  22919  hmeoqtop  22924  cmphmph  22937  connhmph  22938  nrmhmph  22943  indishmph  22947  cmphaushmeo  22949  xpstps  22959  xpstopnlem2  22960  fmid  23109  tsmsf1o  23294  imasdsf1olem  23524  imasf1oxmet  23526  imasf1omet  23527  xpsdsfn  23528  imasf1oxms  23643  imasf1oms  23644  iccpnfhmeo  24106  cnheiborlem  24115  ovolctb  24652  ovolicc2lem4  24682  dyadmbl  24762  mbfimaopnlem  24817  itg1addlem4  24861  itg1addlem4OLD  24862  dvcnvrelem2  25180  dvcnvre  25181  deg1ldg  25255  deg1leb  25258  efifo  25701  logrn  25712  dvrelog  25790  efopnlem2  25810  fsumdvdsmul  26342  f1otrg  27230  axcontlem10  27339  edgusgrnbfin  27738  eupthvdres  28595  cnvunop  30276  counop  30279  idunop  30336  elunop2  30371  fmptco1f1o  30964  padct  31050  symgcom  31348  cycpmconjvlem  31404  cycpmconjslem2  31418  xrge0iifiso  31881  volmeas  32195  ballotlemro  32485  derangenlem  33129  subfacp1lem3  33140  subfacp1lem5  33142  erdsze2lem1  33161  cvmsss2  33232  poimirlem1  35774  poimirlem2  35775  poimirlem3  35776  poimirlem4  35777  poimirlem5  35778  poimirlem6  35779  poimirlem7  35780  poimirlem9  35782  poimirlem10  35783  poimirlem11  35784  poimirlem12  35785  poimirlem14  35787  poimirlem15  35788  poimirlem16  35789  poimirlem17  35790  poimirlem19  35792  poimirlem20  35793  poimirlem22  35795  poimirlem23  35796  poimirlem24  35797  poimirlem25  35798  poimirlem29  35802  poimirlem31  35804  mblfinlem2  35811  ismtybndlem  35960  ismtyres  35962  diaintclN  39068  dibintclN  39177  mapdrn  39659  dnnumch2  40867  kelac1  40885  lnmlmic  40910  pwslnmlem1  40914  pwfi2f1o  40918  gicabl  40921  imasgim  40922  isnumbasgrplem1  40923  ntrneifv2  41660  stoweidlem27  43539  fourierdlem20  43639  fourierdlem51  43669  fourierdlem52  43670  fourierdlem63  43681  fourierdlem64  43682  fourierdlem65  43683  fourierdlem102  43720  fourierdlem114  43732  sge0f1o  43891  nnfoctbdjlem  43964  isomenndlem  44039  ovnsubaddlem1  44079  f1oresf1o2  44751  isomuspgrlem2d  45252