Theorem f1ofo 6787

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

Syntax hints:   → wi 4  ^◡ccnv 5630  Fun wfun 6492  –onto→wfo 6496  –1-1-onto→wf1o 6497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-cleq 2728  df-ss 3906  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505

This theorem is referenced by:  f1imacnv  6796  resin  6802  f1ococnv2  6807  fo00  6816  f1ounsn  7227  f1ocoima  7258  isoini  7293  isofrlem  7295  isoselem  7296  ncanth  7322  f1opw2  7622  f1dmex  7910  f1ovv  7911  f1oweALT  7925  wemoiso2  7927  mptcnfimad  7939  curry1  8054  curry2  8057  smoiso2  8309  f1osetex  8806  bren  8903  f1oeng  8917  en1  8971  canth2  9068  domss2  9074  mapen  9079  ssenen  9089  dif1enlem  9094  ssfiALT  9108  phplem2  9139  php3  9143  f1fi  9224  domunfican  9232  fiint  9237  f1opwfi  9266  mapfien  9321  supisolem  9387  ordiso2  9430  ordtypelem10  9442  oismo  9455  wdomref  9487  brwdom2  9488  unxpwdom2  9503  cantnflt2  9594  cantnfp1lem3  9601  wemapwe  9618  infxpenc2lem1  9941  fseqen  9949  infpwfien  9984  infmap2  10139  ackbij2  10164  cff1  10180  cofsmo  10191  infpssr  10230  enfin2i  10243  fin23lem27  10250  enfin1ai  10306  fin1a2lem7  10328  axcclem  10379  ttukeylem1  10431  fpwwe2lem5  10558  fpwwe2lem8  10561  canthp1lem2  10576  tskuni  10706  gruen  10735  cnexALT  12936  fiinfnf1o  14312  hasheqf1oi  14313  hashfacen  14416  fsumf1o  15685  fsumss  15687  fprodf1o  15911  fprodss  15913  ruc  16210  unbenlem  16879  xpsfrn  17532  xpsbas  17536  xpsadd  17538  xpsmul  17539  xpssca  17540  xpsvsca  17541  xpsless  17542  xpsle  17543  imasmndf1  18744  sursubmefmnd  18864  imasgrpf1  19033  gicsubgen  19254  symgmov2  19363  symgextfo  19397  symgfixelsi  19410  giccyg  19875  gsumzres  19884  gsumzcl2  19885  gsumzf1o  19887  gsumzaddlem  19896  gsumconst  19909  gsumzmhm  19912  gsumzoppg  19919  dprdf1o  20009  imasrngf1  20159  imasringf1  20311  gsumfsum  21414  znleval  21534  lmimlbs  21816  lbslcic  21821  coe1mul2lem2  22233  cmpfi  23373  idqtop  23671  basqtop  23676  tgqtop  23677  hmeontr  23734  hmeoimaf1o  23735  hmeoqtop  23740  cmphmph  23753  connhmph  23754  nrmhmph  23759  indishmph  23763  cmphaushmeo  23765  xpstps  23775  xpstopnlem2  23776  fmid  23925  tsmsf1o  24110  imasdsf1olem  24338  imasf1oxmet  24340  imasf1omet  24341  xpsdsfn  24342  imasf1oxms  24454  imasf1oms  24455  iccpnfhmeo  24912  cnheiborlem  24921  ovolctb  25457  ovolicc2lem4  25487  dyadmbl  25567  mbfimaopnlem  25622  itg1addlem4  25666  dvcnvrelem2  25985  dvcnvre  25986  deg1ldg  26057  deg1leb  26060  efifo  26511  logrn  26522  dvrelog  26601  efopnlem2  26621  fsumdvdsmul  27158  f1otrg  28939  axcontlem10  29042  edgusgrnbfin  29442  eupthvdres  30305  cnvunop  31989  counop  31992  idunop  32049  elunop2  32084  fmptco1f1o  32706  padct  32791  mndlactf1o  33090  mndractf1o  33091  symgcom  33144  cycpmconjvlem  33202  cycpmconjslem2  33216  1arithidomlem2  33596  esplysply  33715  xrge0iifiso  34079  volmeas  34375  ballotlemro  34667  derangenlem  35353  subfacp1lem3  35364  subfacp1lem5  35366  erdsze2lem1  35385  cvmsss2  35456  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem9  37950  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem29  37970  poimirlem31  37972  mblfinlem2  37979  ismtybndlem  38127  ismtyres  38129  diaintclN  41504  dibintclN  41613  mapdrn  42095  aks6d1c1p5  42551  riccrng1  42966  ricdrng1  42973  dnnumch2  43473  kelac1  43491  lnmlmic  43516  pwslnmlem1  43520  pwfi2f1o  43524  gicabl  43527  imasgim  43528  isnumbasgrplem1  43529  ntrneifv2  44507  stoweidlem27  46455  fourierdlem20  46555  fourierdlem51  46585  fourierdlem52  46586  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem102  46636  fourierdlem114  46648  sge0f1o  46810  nnfoctbdjlem  46883  isomenndlem  46958  ovnsubaddlem1  46998  3f1oss1  47523  f1oresf1o2  47739  grimuhgr  48363  grimcnv  48364  isuspgrimlem  48371  grimedg  48411  isubgr3stgrlem8  48449  tposres3  49356  uptrlem1  49685  lmdran  50146  cmdlan  50147