Theorem f1ofo 6807

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

Syntax hints:   → wi 4  ^◡ccnv 5637  Fun wfun 6505  –onto→wfo 6509  –1-1-onto→wf1o 6510

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-cleq 2721  df-ss 3931  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518

This theorem is referenced by:  f1imacnv  6816  resin  6822  f1ococnv2  6827  fo00  6836  f1ounsn  7247  f1ocoima  7278  isoini  7313  isofrlem  7315  isoselem  7316  ncanth  7342  f1opw2  7644  f1dmex  7935  f1ovv  7936  f1oweALT  7951  wemoiso2  7953  mptcnfimad  7965  curry1  8083  curry2  8086  smoiso2  8338  f1osetex  8832  bren  8928  f1oeng  8942  en1  8995  canth2  9094  domss2  9100  mapen  9105  ssenen  9115  dif1enlem  9120  dif1enlemOLD  9121  ssfiALT  9138  phplem2  9169  php3  9173  f1fi  9263  domunfican  9272  fiint  9277  fiintOLD  9278  f1opwfi  9307  mapfien  9359  supisolem  9425  ordiso2  9468  ordtypelem10  9480  oismo  9493  wdomref  9525  brwdom2  9526  unxpwdom2  9541  cantnflt2  9626  cantnfp1lem3  9633  wemapwe  9650  infxpenc2lem1  9972  fseqen  9980  infpwfien  10015  infmap2  10170  ackbij2  10195  cff1  10211  cofsmo  10222  infpssr  10261  enfin2i  10274  fin23lem27  10281  enfin1ai  10337  fin1a2lem7  10359  axcclem  10410  ttukeylem1  10462  fpwwe2lem5  10588  fpwwe2lem8  10591  canthp1lem2  10606  tskuni  10736  gruen  10765  cnexALT  12945  fiinfnf1o  14315  hasheqf1oi  14316  hashfacen  14419  fsumf1o  15689  fsumss  15691  fprodf1o  15912  fprodss  15914  ruc  16211  unbenlem  16879  xpsfrn  17531  xpsbas  17535  xpsadd  17537  xpsmul  17538  xpssca  17539  xpsvsca  17540  xpsless  17541  xpsle  17542  imasmndf1  18703  sursubmefmnd  18823  imasgrpf1  18989  gicsubgen  19211  symgmov2  19318  symgextfo  19352  symgfixelsi  19365  giccyg  19830  gsumzres  19839  gsumzcl2  19840  gsumzf1o  19842  gsumzaddlem  19851  gsumconst  19864  gsumzmhm  19867  gsumzoppg  19874  dprdf1o  19964  imasrngf1  20087  imasringf1  20240  gsumfsum  21351  znleval  21464  lmimlbs  21745  lbslcic  21750  coe1mul2lem2  22154  cmpfi  23295  idqtop  23593  basqtop  23598  tgqtop  23599  hmeontr  23656  hmeoimaf1o  23657  hmeoqtop  23662  cmphmph  23675  connhmph  23676  nrmhmph  23681  indishmph  23685  cmphaushmeo  23687  xpstps  23697  xpstopnlem2  23698  fmid  23847  tsmsf1o  24032  imasdsf1olem  24261  imasf1oxmet  24263  imasf1omet  24264  xpsdsfn  24265  imasf1oxms  24377  imasf1oms  24378  iccpnfhmeo  24843  cnheiborlem  24853  ovolctb  25391  ovolicc2lem4  25421  dyadmbl  25501  mbfimaopnlem  25556  itg1addlem4  25600  dvcnvrelem2  25923  dvcnvre  25924  deg1ldg  25997  deg1leb  26000  efifo  26456  logrn  26467  dvrelog  26546  efopnlem2  26566  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  f1otrg  28798  axcontlem10  28900  edgusgrnbfin  29300  eupthvdres  30164  cnvunop  31847  counop  31850  idunop  31907  elunop2  31942  fmptco1f1o  32557  padct  32643  mndlactf1o  32971  mndractf1o  32972  symgcom  33040  cycpmconjvlem  33098  cycpmconjslem2  33112  1arithidomlem2  33507  xrge0iifiso  33925  volmeas  34221  ballotlemro  34514  derangenlem  35158  subfacp1lem3  35169  subfacp1lem5  35171  erdsze2lem1  35190  cvmsss2  35261  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem9  37623  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem29  37643  poimirlem31  37645  mblfinlem2  37652  ismtybndlem  37800  ismtyres  37802  diaintclN  41052  dibintclN  41161  mapdrn  41643  aks6d1c1p5  42100  riccrng1  42509  ricdrng1  42516  dnnumch2  43034  kelac1  43052  lnmlmic  43077  pwslnmlem1  43081  pwfi2f1o  43085  gicabl  43088  imasgim  43089  isnumbasgrplem1  43090  ntrneifv2  44069  stoweidlem27  46025  fourierdlem20  46125  fourierdlem51  46155  fourierdlem52  46156  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem102  46206  fourierdlem114  46218  sge0f1o  46380  nnfoctbdjlem  46453  isomenndlem  46528  ovnsubaddlem1  46568  3f1oss1  47076  f1oresf1o2  47292  grimuhgr  47887  grimcnv  47888  isuspgrimlem  47895  grimedg  47935  isubgr3stgrlem8  47972  tposres3  48869  uptrlem1  49199  lmdran  49660  cmdlan  49661