Theorem f1ofo 6828

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

Syntax hints:   → wi 4  ^◡ccnv 5660  Fun wfun 6530  –onto→wfo 6534  –1-1-onto→wf1o 6535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-ex 1810  df-cleq 2755  df-ss 3922  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543

This theorem is referenced by:  f1imacnv  6837  resin  6843  f1ococnv2  6848  fo00  6857  f1ounsn  7270  f1ocoima  7301  isoini  7336  isofrlem  7338  isoselem  7339  ncanth  7365  f1opw2  7665  f1dmex  7950  f1ovv  7951  f1oweALT  7965  wemoiso2  7967  mptcnfimad  7979  curry1  8095  curry2  8098  smoiso2  8352  f1osetex  8852  bren  8949  f1oeng  8963  en1  9017  canth2  9114  domss2  9120  mapen  9125  ssenen  9135  dif1enlem  9140  ssfiALT  9154  phplem2  9185  php3  9189  f1fi  9270  domunfican  9277  fiint  9282  f1opwfi  9309  mapfien  9364  supisolem  9430  ordiso2  9473  ordtypelem10  9485  oismo  9498  wdomref  9530  brwdom2  9531  unxpwdom2  9546  cantnflt2  9638  cantnfp1lem3  9645  wemapwe  9662  infxpenc2lem1  9999  fseqen  10007  infpwfien  10042  infmap2  10196  ackbij2  10221  cff1  10237  cofsmo  10248  infpssr  10287  enfin2i  10300  fin23lem27  10307  enfin1ai  10363  fin1a2lem7  10385  axcclem  10436  ttukeylem1  10488  fpwwe2lem5  10615  fpwwe2lem8  10618  canthp1lem2  10633  tskuni  10763  gruen  10792  cnexALT  13005  fiinfnf1o  14382  hasheqf1oi  14383  hashfacen  14487  fsumf1o  15770  fsumss  15772  fprodf1o  15996  fprodss  15998  ruc  16294  unbenlem  16963  xpsfrn  17617  xpsbas  17621  xpsadd  17623  xpsmul  17624  xpssca  17625  xpsvsca  17626  xpsless  17627  xpsle  17628  imasmndf1  18829  sursubmefmnd  18950  imasgrpf1  19118  gicsubgen  19344  symgmov2  19453  symgextfo  19487  symgfixelsi  19500  giccyg  19965  gsumzres  19974  gsumzcl2  19975  gsumzf1o  19977  gsumzaddlem  19986  gsumconst  19999  gsumzmhm  20002  gsumzoppg  20009  dprdf1o  20099  imasrngf1  20251  imasringf1  20409  gsumfsum  21584  znleval  21704  lmimlbs  21986  lbslcic  21991  coe1mul2lem2  22429  cmpfi  23565  idqtop  23863  basqtop  23868  tgqtop  23869  hmeontr  23926  hmeoimaf1o  23927  hmeoqtop  23932  cmphmph  23945  connhmph  23946  nrmhmph  23951  indishmph  23955  cmphaushmeo  23957  xpstps  23967  xpstopnlem2  23968  fmid  24117  tsmsf1o  24302  imasdsf1olem  24530  imasf1oxmet  24532  imasf1omet  24533  xpsdsfn  24534  imasf1oxms  24646  imasf1oms  24647  iccpnfhmeo  25104  cnheiborlem  25113  ovolctb  25649  ovolicc2lem4  25679  dyadmbl  25759  mbfimaopnlem  25814  itg1addlem4  25858  dvcnvrelem2  26177  dvcnvre  26178  deg1ldg  26249  deg1leb  26252  efifo  26712  logrn  26723  dvrelog  26802  efopnlem2  26822  fsumdvdsmul  27359  f1otrg  29220  axcontlem10  29323  edgusgrnbfin  29723  eupthvdres  30586  cnvunop  32270  counop  32273  idunop  32330  elunop2  32365  fmptco1f1o  32978  padct  33063  mndlactf1o  33350  mndractf1o  33351  symgcom  33403  cycpmconjvlem  33461  cycpmconjslem2  33475  1arithidomlem2  33826  esplysply  33961  xrge0iifiso  34325  volmeas  34621  ballotlemro  34913  vonf1oonfo  35599  derangenlem  35663  subfacp1lem3  35674  subfacp1lem5  35676  erdsze2lem1  35695  cvmsss2  35766  poimirlem1  38292  poimirlem2  38293  poimirlem3  38294  poimirlem4  38295  poimirlem5  38296  poimirlem6  38297  poimirlem7  38298  poimirlem9  38300  poimirlem10  38301  poimirlem11  38302  poimirlem12  38303  poimirlem14  38305  poimirlem15  38306  poimirlem16  38307  poimirlem17  38308  poimirlem19  38310  poimirlem20  38311  poimirlem22  38313  poimirlem23  38314  poimirlem24  38315  poimirlem25  38316  poimirlem29  38320  poimirlem31  38322  mblfinlem2  38329  ismtybndlem  38477  ismtyres  38479  diaintclN  41852  dibintclN  41961  mapdrn  42443  aks6d1c1p5  42899  riccrng1  43309  ricdrng1  43316  dnnumch2  43792  kelac1  43810  lnmlmic  43835  pwslnmlem1  43839  pwfi2f1o  43843  gicabl  43846  imasgim  43847  isnumbasgrplem1  43848  ntrneifv2  44826  stoweidlem27  46761  fourierdlem20  46861  fourierdlem51  46891  fourierdlem52  46892  fourierdlem63  46903  fourierdlem64  46904  fourierdlem65  46905  fourierdlem102  46942  fourierdlem114  46954  sge0f1o  47116  nnfoctbdjlem  47189  isomenndlem  47264  ovnsubaddlem1  47304  3f1oss1  47832  f1oresf1o2  48048  grimuhgr  48672  grimcnv  48673  isuspgrimlem  48680  grimedg  48720  isubgr3stgrlem8  48758  tposres3  49679  uptrlem1  50008  lmdran  50469  cmdlan  50470