Theorem f1ofo 6855

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

Syntax hints:   → wi 4  ^◡ccnv 5684  Fun wfun 6555  –onto→wfo 6559  –1-1-onto→wf1o 6560

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1780  df-cleq 2729  df-ss 3968  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568

This theorem is referenced by:  f1imacnv  6864  resin  6870  f1ococnv2  6875  fo00  6884  f1ounsn  7292  f1ocoima  7323  isoini  7358  isofrlem  7360  isoselem  7361  ncanth  7386  f1opw2  7688  f1dmex  7981  f1ovv  7982  f1oweALT  7997  wemoiso2  7999  mptcnfimad  8011  curry1  8129  curry2  8132  smoiso2  8409  f1osetex  8899  bren  8995  f1oeng  9011  en1  9064  canth2  9170  domss2  9176  mapen  9181  ssenen  9191  dif1enlem  9196  dif1enlemOLD  9197  ssfiALT  9214  phplem2  9245  php3  9249  phplem4OLD  9257  php3OLD  9261  f1fi  9352  domunfican  9361  fiint  9366  fiintOLD  9367  f1opwfi  9396  mapfien  9448  supisolem  9513  ordiso2  9555  ordtypelem10  9567  oismo  9580  wdomref  9612  brwdom2  9613  unxpwdom2  9628  cantnflt2  9713  cantnfp1lem3  9720  wemapwe  9737  infxpenc2lem1  10059  fseqen  10067  infpwfien  10102  infmap2  10257  ackbij2  10282  cff1  10298  cofsmo  10309  infpssr  10348  enfin2i  10361  fin23lem27  10368  enfin1ai  10424  fin1a2lem7  10446  axcclem  10497  ttukeylem1  10549  fpwwe2lem5  10675  fpwwe2lem8  10678  canthp1lem2  10693  tskuni  10823  gruen  10852  cnexALT  13028  fiinfnf1o  14389  hasheqf1oi  14390  hashfacen  14493  fsumf1o  15759  fsumss  15761  fprodf1o  15982  fprodss  15984  ruc  16279  unbenlem  16946  xpsfrn  17613  xpsbas  17617  xpsadd  17619  xpsmul  17620  xpssca  17621  xpsvsca  17622  xpsless  17623  xpsle  17624  imasmndf1  18789  sursubmefmnd  18909  imasgrpf1  19075  gicsubgen  19297  symgmov2  19405  symgextfo  19440  symgfixelsi  19453  giccyg  19918  gsumzres  19927  gsumzcl2  19928  gsumzf1o  19930  gsumzaddlem  19939  gsumconst  19952  gsumzmhm  19955  gsumzoppg  19962  dprdf1o  20052  imasrngf1  20175  imasringf1  20328  gsumfsum  21452  znleval  21573  lmimlbs  21856  lbslcic  21861  coe1mul2lem2  22271  cmpfi  23416  idqtop  23714  basqtop  23719  tgqtop  23720  hmeontr  23777  hmeoimaf1o  23778  hmeoqtop  23783  cmphmph  23796  connhmph  23797  nrmhmph  23802  indishmph  23806  cmphaushmeo  23808  xpstps  23818  xpstopnlem2  23819  fmid  23968  tsmsf1o  24153  imasdsf1olem  24383  imasf1oxmet  24385  imasf1omet  24386  xpsdsfn  24387  imasf1oxms  24502  imasf1oms  24503  iccpnfhmeo  24976  cnheiborlem  24986  ovolctb  25525  ovolicc2lem4  25555  dyadmbl  25635  mbfimaopnlem  25690  itg1addlem4  25734  dvcnvrelem2  26057  dvcnvre  26058  deg1ldg  26131  deg1leb  26134  efifo  26589  logrn  26600  dvrelog  26679  efopnlem2  26699  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  f1otrg  28879  axcontlem10  28988  edgusgrnbfin  29390  eupthvdres  30254  cnvunop  31937  counop  31940  idunop  31997  elunop2  32032  fmptco1f1o  32643  padct  32731  mndlactf1o  33035  mndractf1o  33036  symgcom  33103  cycpmconjvlem  33161  cycpmconjslem2  33175  1arithidomlem2  33564  xrge0iifiso  33934  volmeas  34232  ballotlemro  34525  derangenlem  35176  subfacp1lem3  35187  subfacp1lem5  35189  erdsze2lem1  35208  cvmsss2  35279  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem9  37636  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem29  37656  poimirlem31  37658  mblfinlem2  37665  ismtybndlem  37813  ismtyres  37815  diaintclN  41060  dibintclN  41169  mapdrn  41651  aks6d1c1p5  42113  riccrng1  42531  ricdrng1  42538  dnnumch2  43057  kelac1  43075  lnmlmic  43100  pwslnmlem1  43104  pwfi2f1o  43108  gicabl  43111  imasgim  43112  isnumbasgrplem1  43113  ntrneifv2  44093  stoweidlem27  46042  fourierdlem20  46142  fourierdlem51  46172  fourierdlem52  46173  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem102  46223  fourierdlem114  46235  sge0f1o  46397  nnfoctbdjlem  46470  isomenndlem  46545  ovnsubaddlem1  46585  3f1oss1  47087  f1oresf1o2  47303  uspgrimprop  47873  isuspgrimlem  47874  grimuhgr  47878  grimcnv  47879  grimedg  47903  isubgr3stgrlem8  47940  tposres3  48781