Theorem f1ofo 6824

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

Syntax hints:   → wi 4  ^◡ccnv 5653  Fun wfun 6524  –onto→wfo 6528  –1-1-onto→wf1o 6529

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-cleq 2727  df-ss 3943  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537

This theorem is referenced by:  f1imacnv  6833  resin  6839  f1ococnv2  6844  fo00  6853  f1ounsn  7264  f1ocoima  7295  isoini  7330  isofrlem  7332  isoselem  7333  ncanth  7358  f1opw2  7660  f1dmex  7953  f1ovv  7954  f1oweALT  7969  wemoiso2  7971  mptcnfimad  7983  curry1  8101  curry2  8104  smoiso2  8381  f1osetex  8871  bren  8967  f1oeng  8983  en1  9036  canth2  9142  domss2  9148  mapen  9153  ssenen  9163  dif1enlem  9168  dif1enlemOLD  9169  ssfiALT  9186  phplem2  9217  php3  9221  php3OLD  9231  f1fi  9322  domunfican  9331  fiint  9336  fiintOLD  9337  f1opwfi  9366  mapfien  9418  supisolem  9484  ordiso2  9527  ordtypelem10  9539  oismo  9552  wdomref  9584  brwdom2  9585  unxpwdom2  9600  cantnflt2  9685  cantnfp1lem3  9692  wemapwe  9709  infxpenc2lem1  10031  fseqen  10039  infpwfien  10074  infmap2  10229  ackbij2  10254  cff1  10270  cofsmo  10281  infpssr  10320  enfin2i  10333  fin23lem27  10340  enfin1ai  10396  fin1a2lem7  10418  axcclem  10469  ttukeylem1  10521  fpwwe2lem5  10647  fpwwe2lem8  10650  canthp1lem2  10665  tskuni  10795  gruen  10824  cnexALT  13000  fiinfnf1o  14366  hasheqf1oi  14367  hashfacen  14470  fsumf1o  15737  fsumss  15739  fprodf1o  15960  fprodss  15962  ruc  16259  unbenlem  16926  xpsfrn  17580  xpsbas  17584  xpsadd  17586  xpsmul  17587  xpssca  17588  xpsvsca  17589  xpsless  17590  xpsle  17591  imasmndf1  18752  sursubmefmnd  18872  imasgrpf1  19038  gicsubgen  19260  symgmov2  19367  symgextfo  19401  symgfixelsi  19414  giccyg  19879  gsumzres  19888  gsumzcl2  19889  gsumzf1o  19891  gsumzaddlem  19900  gsumconst  19913  gsumzmhm  19916  gsumzoppg  19923  dprdf1o  20013  imasrngf1  20136  imasringf1  20289  gsumfsum  21400  znleval  21513  lmimlbs  21794  lbslcic  21799  coe1mul2lem2  22203  cmpfi  23344  idqtop  23642  basqtop  23647  tgqtop  23648  hmeontr  23705  hmeoimaf1o  23706  hmeoqtop  23711  cmphmph  23724  connhmph  23725  nrmhmph  23730  indishmph  23734  cmphaushmeo  23736  xpstps  23746  xpstopnlem2  23747  fmid  23896  tsmsf1o  24081  imasdsf1olem  24310  imasf1oxmet  24312  imasf1omet  24313  xpsdsfn  24314  imasf1oxms  24426  imasf1oms  24427  iccpnfhmeo  24892  cnheiborlem  24902  ovolctb  25441  ovolicc2lem4  25471  dyadmbl  25551  mbfimaopnlem  25606  itg1addlem4  25650  dvcnvrelem2  25973  dvcnvre  25974  deg1ldg  26047  deg1leb  26050  efifo  26506  logrn  26517  dvrelog  26596  efopnlem2  26616  fsumdvdsmul  27155  fsumdvdsmulOLD  27157  f1otrg  28796  axcontlem10  28898  edgusgrnbfin  29298  eupthvdres  30162  cnvunop  31845  counop  31848  idunop  31905  elunop2  31940  fmptco1f1o  32557  padct  32643  mndlactf1o  32971  mndractf1o  32972  symgcom  33040  cycpmconjvlem  33098  cycpmconjslem2  33112  1arithidomlem2  33497  xrge0iifiso  33912  volmeas  34208  ballotlemro  34501  derangenlem  35139  subfacp1lem3  35150  subfacp1lem5  35152  erdsze2lem1  35171  cvmsss2  35242  poimirlem1  37591  poimirlem2  37592  poimirlem3  37593  poimirlem4  37594  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem9  37599  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem14  37604  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem22  37612  poimirlem23  37613  poimirlem24  37614  poimirlem25  37615  poimirlem29  37619  poimirlem31  37621  mblfinlem2  37628  ismtybndlem  37776  ismtyres  37778  diaintclN  41023  dibintclN  41132  mapdrn  41614  aks6d1c1p5  42071  riccrng1  42491  ricdrng1  42498  dnnumch2  43016  kelac1  43034  lnmlmic  43059  pwslnmlem1  43063  pwfi2f1o  43067  gicabl  43070  imasgim  43071  isnumbasgrplem1  43072  ntrneifv2  44051  stoweidlem27  46004  fourierdlem20  46104  fourierdlem51  46134  fourierdlem52  46135  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem102  46185  fourierdlem114  46197  sge0f1o  46359  nnfoctbdjlem  46432  isomenndlem  46507  ovnsubaddlem1  46547  3f1oss1  47052  f1oresf1o2  47268  grimuhgr  47848  grimcnv  47849  isuspgrimlem  47856  grimedg  47896  isubgr3stgrlem8  47933  tposres3  48804