Theorem f1ofo 6810

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

Syntax hints:   → wi 4  ^◡ccnv 5640  Fun wfun 6508  –onto→wfo 6512  –1-1-onto→wf1o 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-cleq 2722  df-ss 3934  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521

This theorem is referenced by:  f1imacnv  6819  resin  6825  f1ococnv2  6830  fo00  6839  f1ounsn  7250  f1ocoima  7281  isoini  7316  isofrlem  7318  isoselem  7319  ncanth  7345  f1opw2  7647  f1dmex  7938  f1ovv  7939  f1oweALT  7954  wemoiso2  7956  mptcnfimad  7968  curry1  8086  curry2  8089  smoiso2  8341  f1osetex  8835  bren  8931  f1oeng  8945  en1  8998  canth2  9100  domss2  9106  mapen  9111  ssenen  9121  dif1enlem  9126  dif1enlemOLD  9127  ssfiALT  9144  phplem2  9175  php3  9179  f1fi  9270  domunfican  9279  fiint  9284  fiintOLD  9285  f1opwfi  9314  mapfien  9366  supisolem  9432  ordiso2  9475  ordtypelem10  9487  oismo  9500  wdomref  9532  brwdom2  9533  unxpwdom2  9548  cantnflt2  9633  cantnfp1lem3  9640  wemapwe  9657  infxpenc2lem1  9979  fseqen  9987  infpwfien  10022  infmap2  10177  ackbij2  10202  cff1  10218  cofsmo  10229  infpssr  10268  enfin2i  10281  fin23lem27  10288  enfin1ai  10344  fin1a2lem7  10366  axcclem  10417  ttukeylem1  10469  fpwwe2lem5  10595  fpwwe2lem8  10598  canthp1lem2  10613  tskuni  10743  gruen  10772  cnexALT  12952  fiinfnf1o  14322  hasheqf1oi  14323  hashfacen  14426  fsumf1o  15696  fsumss  15698  fprodf1o  15919  fprodss  15921  ruc  16218  unbenlem  16886  xpsfrn  17538  xpsbas  17542  xpsadd  17544  xpsmul  17545  xpssca  17546  xpsvsca  17547  xpsless  17548  xpsle  17549  imasmndf1  18710  sursubmefmnd  18830  imasgrpf1  18996  gicsubgen  19218  symgmov2  19325  symgextfo  19359  symgfixelsi  19372  giccyg  19837  gsumzres  19846  gsumzcl2  19847  gsumzf1o  19849  gsumzaddlem  19858  gsumconst  19871  gsumzmhm  19874  gsumzoppg  19881  dprdf1o  19971  imasrngf1  20094  imasringf1  20247  gsumfsum  21358  znleval  21471  lmimlbs  21752  lbslcic  21757  coe1mul2lem2  22161  cmpfi  23302  idqtop  23600  basqtop  23605  tgqtop  23606  hmeontr  23663  hmeoimaf1o  23664  hmeoqtop  23669  cmphmph  23682  connhmph  23683  nrmhmph  23688  indishmph  23692  cmphaushmeo  23694  xpstps  23704  xpstopnlem2  23705  fmid  23854  tsmsf1o  24039  imasdsf1olem  24268  imasf1oxmet  24270  imasf1omet  24271  xpsdsfn  24272  imasf1oxms  24384  imasf1oms  24385  iccpnfhmeo  24850  cnheiborlem  24860  ovolctb  25398  ovolicc2lem4  25428  dyadmbl  25508  mbfimaopnlem  25563  itg1addlem4  25607  dvcnvrelem2  25930  dvcnvre  25931  deg1ldg  26004  deg1leb  26007  efifo  26463  logrn  26474  dvrelog  26553  efopnlem2  26573  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  f1otrg  28805  axcontlem10  28907  edgusgrnbfin  29307  eupthvdres  30171  cnvunop  31854  counop  31857  idunop  31914  elunop2  31949  fmptco1f1o  32564  padct  32650  mndlactf1o  32978  mndractf1o  32979  symgcom  33047  cycpmconjvlem  33105  cycpmconjslem2  33119  1arithidomlem2  33514  xrge0iifiso  33932  volmeas  34228  ballotlemro  34521  derangenlem  35165  subfacp1lem3  35176  subfacp1lem5  35178  erdsze2lem1  35197  cvmsss2  35268  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem9  37630  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem14  37635  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem29  37650  poimirlem31  37652  mblfinlem2  37659  ismtybndlem  37807  ismtyres  37809  diaintclN  41059  dibintclN  41168  mapdrn  41650  aks6d1c1p5  42107  riccrng1  42516  ricdrng1  42523  dnnumch2  43041  kelac1  43059  lnmlmic  43084  pwslnmlem1  43088  pwfi2f1o  43092  gicabl  43095  imasgim  43096  isnumbasgrplem1  43097  ntrneifv2  44076  stoweidlem27  46032  fourierdlem20  46132  fourierdlem51  46162  fourierdlem52  46163  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem102  46213  fourierdlem114  46225  sge0f1o  46387  nnfoctbdjlem  46460  isomenndlem  46535  ovnsubaddlem1  46575  3f1oss1  47080  f1oresf1o2  47296  grimuhgr  47891  grimcnv  47892  isuspgrimlem  47899  grimedg  47939  isubgr3stgrlem8  47976  tposres3  48873  uptrlem1  49203  lmdran  49664  cmdlan  49665