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 5687  Fun wfun 6556  –onto→wfo 6560  –1-1-onto→wf1o 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1776  df-cleq 2726  df-ss 3979  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569

This theorem is referenced by:  f1imacnv  6864  resin  6870  f1ococnv2  6875  fo00  6884  f1ounsn  7291  f1ocoima  7322  isoini  7357  isofrlem  7359  isoselem  7360  ncanth  7385  f1opw2  7687  f1dmex  7979  f1ovv  7980  f1oweALT  7995  wemoiso2  7997  mptcnfimad  8009  curry1  8127  curry2  8130  smoiso2  8407  f1osetex  8897  bren  8993  f1oeng  9009  en1  9062  canth2  9168  domss2  9174  mapen  9179  ssenen  9189  dif1enlem  9194  dif1enlemOLD  9195  ssfiALT  9212  phplem2  9242  php3  9246  phplem4OLD  9254  php3OLD  9258  f1fi  9349  domunfican  9358  fiint  9363  fiintOLD  9364  f1opwfi  9393  mapfien  9445  supisolem  9510  ordiso2  9552  ordtypelem10  9564  oismo  9577  wdomref  9609  brwdom2  9610  unxpwdom2  9625  cantnflt2  9710  cantnfp1lem3  9717  wemapwe  9734  infxpenc2lem1  10056  fseqen  10064  infpwfien  10099  infmap2  10254  ackbij2  10279  cff1  10295  cofsmo  10306  infpssr  10345  enfin2i  10358  fin23lem27  10365  enfin1ai  10421  fin1a2lem7  10443  axcclem  10494  ttukeylem1  10546  fpwwe2lem5  10672  fpwwe2lem8  10675  canthp1lem2  10690  tskuni  10820  gruen  10849  cnexALT  13025  fiinfnf1o  14385  hasheqf1oi  14386  hashfacen  14489  fsumf1o  15755  fsumss  15757  fprodf1o  15978  fprodss  15980  ruc  16275  unbenlem  16941  xpsfrn  17614  xpsbas  17618  xpsadd  17620  xpsmul  17621  xpssca  17622  xpsvsca  17623  xpsless  17624  xpsle  17625  imasmndf1  18801  sursubmefmnd  18921  imasgrpf1  19087  gicsubgen  19309  symgmov2  19419  symgextfo  19454  symgfixelsi  19467  giccyg  19932  gsumzres  19941  gsumzcl2  19942  gsumzf1o  19944  gsumzaddlem  19953  gsumconst  19966  gsumzmhm  19969  gsumzoppg  19976  dprdf1o  20066  imasrngf1  20195  imasringf1  20344  gsumfsum  21469  znleval  21590  lmimlbs  21873  lbslcic  21878  coe1mul2lem2  22286  cmpfi  23431  idqtop  23729  basqtop  23734  tgqtop  23735  hmeontr  23792  hmeoimaf1o  23793  hmeoqtop  23798  cmphmph  23811  connhmph  23812  nrmhmph  23817  indishmph  23821  cmphaushmeo  23823  xpstps  23833  xpstopnlem2  23834  fmid  23983  tsmsf1o  24168  imasdsf1olem  24398  imasf1oxmet  24400  imasf1omet  24401  xpsdsfn  24402  imasf1oxms  24517  imasf1oms  24518  iccpnfhmeo  24989  cnheiborlem  24999  ovolctb  25538  ovolicc2lem4  25568  dyadmbl  25648  mbfimaopnlem  25703  itg1addlem4  25747  itg1addlem4OLD  25748  dvcnvrelem2  26071  dvcnvre  26072  deg1ldg  26145  deg1leb  26148  efifo  26603  logrn  26614  dvrelog  26693  efopnlem2  26713  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  f1otrg  28893  axcontlem10  29002  edgusgrnbfin  29404  eupthvdres  30263  cnvunop  31946  counop  31949  idunop  32006  elunop2  32041  fmptco1f1o  32649  padct  32736  mndlactf1o  33017  mndractf1o  33018  symgcom  33085  cycpmconjvlem  33143  cycpmconjslem2  33157  1arithidomlem2  33543  xrge0iifiso  33895  volmeas  34211  ballotlemro  34503  derangenlem  35155  subfacp1lem3  35166  subfacp1lem5  35168  erdsze2lem1  35187  cvmsss2  35258  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem9  37615  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem29  37635  poimirlem31  37637  mblfinlem2  37644  ismtybndlem  37792  ismtyres  37794  diaintclN  41040  dibintclN  41149  mapdrn  41631  aks6d1c1p5  42093  riccrng1  42507  ricdrng1  42514  dnnumch2  43033  kelac1  43051  lnmlmic  43076  pwslnmlem1  43080  pwfi2f1o  43084  gicabl  43087  imasgim  43088  isnumbasgrplem1  43089  ntrneifv2  44069  stoweidlem27  45982  fourierdlem20  46082  fourierdlem51  46112  fourierdlem52  46113  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem102  46163  fourierdlem114  46175  sge0f1o  46337  nnfoctbdjlem  46410  isomenndlem  46485  ovnsubaddlem1  46525  3f1oss1  47024  f1oresf1o2  47240  uspgrimprop  47810  isuspgrimlem  47811  grimuhgr  47815  grimcnv  47816  grimedg  47840  isubgr3stgrlem8  47875