Theorem f1of 6810

Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1of	⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Proof of Theorem f1of

Step	Hyp	Ref	Expression
1		f1of1 6809	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
2		f1f 6764	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
3	1, 2	syl 18	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ⟶wf 6521  –1-1→wf1 6522  –1-1-onto→wf1o 6524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401  df-f1 6530  df-f1o 6532

This theorem is referenced by:  f1ofn  6811  f1ompt  7096  f1oresrab  7113  fsn  7121  fsnunf  7173  f1ounsn  7260  f1ocnvfv1  7264  f1ocnvfv2  7265  fsnex  7271  f1ocnvdm  7273  fcof1oinvd  7281  fveqf1o  7290  isocnv  7318  isocnv3  7320  isores2  7321  isotr  7324  isofr2  7332  isopolem  7333  isosolem  7335  f1oiso2  7340  weniso  7342  f1ofveu  7394  f1oexrnex  7912  f1oabexg  7926  wemoiso  7958  mptcnfimad  7971  suppsnop  8162  smoiso  8337  mapsnd  8872  ralxpmap  8882  f1oen2g  8953  en1  9009  enfixsn  9062  mapen  9117  ac6sfi  9232  domunfican  9269  fiint  9274  mapfienlem1  9353  mapfienlem2  9354  mapfienlem3  9355  mapfien  9356  supisoex  9423  supiso  9424  ordiso2  9465  unxpwdom2  9538  cantnfle  9628  cantnfp1lem3  9637  cantnflem1b  9643  cantnflem1d  9645  cantnflem1  9646  cnfcomlem  9656  cnfcom  9657  cnfcom2lem  9658  cnfcom2  9659  cnfcom3lem  9660  cnfcom3  9661  cnfcom3clem  9662  djuin  9892  infxpenlem  9985  infxpenc  9990  infxpenc2lem2  9992  fseqenlem1  9996  acndom  10023  acndom2  10026  infpwfien  10034  iunfictbso  10086  infmap2  10188  ackbij2lem2  10210  infpssrlem3  10277  infpssrlem4  10278  fin23lem30  10314  isf32lem6  10330  isf32lem7  10331  isf32lem8  10332  enfin1ai  10356  axcc3  10410  axcclem  10429  ttukeylem7  10487  fpwwe2lem5  10608  fpwwe2lem6  10609  fpwwe2lem8  10611  canthp1lem2  10626  canthp1  10627  pwfseqlem4a  10634  pwfseqlem5  10636  axdc4uzlem  14010  seqf1olem1  14068  seqf1olem2  14069  seqf1o  14070  hashkf  14359  hasheqf1oi  14378  hasheqf1od  14380  hashcl  14383  hashgadd  14404  hashfacen  14481  hashf1lem1  14482  fz1isolem  14488  seqcoll  14491  seqcoll2  14492  cnrecnv  15206  sumeq2ii  15734  summolem3  15755  summolem2a  15756  fsum  15761  fsumf1o  15764  fsumss  15766  fsumcl2lem  15772  fsumadd  15781  fsummulc2  15825  fsumrelem  15849  ackbijnn  15872  prodeq2ii  15955  prodmolem3  15977  prodmolem2a  15978  fprod  15985  fprodf1o  15990  fprodss  15992  fprodser  15993  fprodcl2lem  15994  fprodmul  16004  fproddiv  16005  fprodn0  16023  fproddvdsd  16383  sadcaddlem  16505  sadadd2lem  16507  sadadd3  16509  sadaddlem  16514  sadasslem  16518  sadeq  16520  phimullem  16828  eulerthlem1  16830  eulerthlem2  16831  unbenlem  16958  vdwlem8  17038  0ram  17070  wunndx  17245  xpsaddlem  17617  xpsvsca  17621  xpsle  17623  idfucl  17928  setccatid  18131  setcinv  18137  catcisolem  18157  estrccatid  18178  funcestrcsetclem7  18192  funcestrcsetclem8  18193  funcsetcestrclem7  18207  funcsetcestrclem8  18208  yonffthlem  18328  gsumpropd2lem  18727  mgmhmf1o  18748  idmgmhm  18749  idmhm  18843  mhmf1o  18844  gsumws1  18887  ielefmnd  18936  idghm  19292  ghmf1o  19309  symgbas  19433  elsymgbas  19435  symgbasf  19437  symgbasfi  19440  symg1bas  19452  symggrp  19461  lactghmga  19466  symgfixf1  19498  f1omvdmvd  19504  f1omvdconj  19507  f1omvdco2  19509  pmtrfconj  19527  symggen  19531  pmtrdifellem1  19537  pmtrdifellem2  19538  psgnunilem1  19554  gsumval3eu  19965  gsumval3lem1  19966  gsumval3  19968  gsumzf1o  19973  gsumconst  19995  gsumsub  20009  gsumcom2  20036  dprdfsub  20084  dprdf1o  20095  dprdsn  20099  ablfaclem2  20149  rngisomfv1  20538  rngisom1  20539  rngisomring1  20541  fidomndrnglem  20845  srngcl  20921  lmhmf1o  21136  gsumfsum  21544  zntoslem  21666  islinds2  21923  lindsmm  21938  psrass1lem  22043  psrnegcl  22064  psrlinv  22065  coe1f2  22329  coe1add  22385  evls1rhmlem  22442  evl1sca  22455  pf1ind  22476  mat1dimelbas  22589  mat1f  22600  mdetleib2  22706  mdetrsca  22721  mdetralt  22726  mdetunilem7  22736  mdetunilem9  22738  ssidcn  23373  hmphdis  23914  indishmph  23916  cmphaushmeo  23918  ordthmeolem  23919  txhmeo  23921  qtopf1  23934  ufldom  24080  symgtgp  24224  tsmsf1o  24263  iducn  24400  imasdsf1olem  24491  xpsdsval  24499  imasf1obl  24606  icchmeo  25061  iccpnfcnv  25064  xrhmeo  25066  cnheiborlem  25074  ovolctb  25610  ovoliunlem1  25622  ovoliunlem2  25623  iunmbl2  25677  dyadmbl  25720  vitalilem2  25729  vitalilem3  25730  vitalilem4  25731  vitalilem5  25732  mbfid  25755  dvid  26038  dvexp  26073  dvcnvlem  26096  dvcnv  26097  dvcnvrelem2  26138  dvcnvre  26139  efcvx  26570  reefgim  26571  efif1olem4  26668  eff1olem  26671  logrncl  26690  relogcl  26698  dvrelog  26760  relogcn  26761  logcn  26770  logf1o2  26773  dvlog  26774  dvlog2  26776  advlog  26777  advlogexp  26778  logtayl  26783  logccv  26786  dvcxp1  26863  loglesqrt  26884  asinrebnd  27024  dvatan  27058  efrlim  27092  amgmlem  27112  lgamcvg2  27177  wilthlem2  27191  wilthlem3  27192  sqff1o  27304  lgsqrlem4  27471  logdivsum  27655  log2sumbnd  27666  isismt  28761  motcl  28766  motco  28767  cnvmot  28768  motgrp  28770  motcgrg  28771  f1otrg  29129  f1otrge  29130  axlowdimlem10  29210  axcontlem5  29227  axcontlem10  29232  uspgriedgedg  29435  upgrres1  29572  umgrres1  29573  upgriseupth  30467  pliguhgr  30747  dmadjrn  32156  unopnorm  32178  unopadj  32180  unoplin  32181  counop  32182  idcnop  32242  idhmop  32243  unopbd  32276  bracnln  32370  cnvbraval  32371  leopnmid  32399  nmopleid  32400  hmopidmch  32414  hmopidmpj  32415  disjrdx  32846  fmptco1f1o  32890  isoun  32959  padct  32975  fcobij  32977  fcobijfs  32978  fcobijfs2  32979  wrdpmcl  33171  ccatws1f1o  33184  ccatws1f1olast  33185  mndlactf1o  33263  mndractf1o  33264  abliso  33268  symgfcoeu  33315  symgcom  33316  pmtrcnel  33322  pmtrcnel2  33323  pmtrcnelor  33324  wrdpmtrlast  33326  cycpmco2f1  33357  cycpmco2rn  33358  cycpmco2lem2  33360  cycpmco2lem3  33361  cycpmco2lem4  33362  cycpmco2lem5  33363  cycpmco2lem6  33364  cycpmco2lem7  33365  cycpmco2  33366  cycpmconjv  33375  cycpmconjslem1  33387  cycpmconjslem2  33388  cycpmconjs  33389  islinds5  33597  ellspds  33598  1arithidomlem1  33742  1arithidomlem2  33743  1arithidom  33744  0mplrim  33821  selvply1rhmlemb  33826  mplvrpmlem  33850  mplvrpmfgalem  33851  mplvrpmmhm  33853  mplvrpmrhm  33854  esplyfval0  33871  esplylem  33873  esplympl  33874  esplymhp  33875  esplyfv1  33876  esplyfv  33877  esplysply  33878  esplyfval3  33879  vieta  33887  tpr2rico  34219  xrge0iifmhm  34246  xrge0pluscn  34247  rrhre  34328  esumf1o  34357  volmeas  34538  eulerpartgbij  34679  eulerpartlemmf  34682  eulerpartlemgvv  34683  eulerpartlemgf  34686  eulerpartlemgs2  34687  eulerpartlemn  34688  ballotlemsima  34823  reprpmtf1o  34930  logdivsqrle  34954  hgt750lemg  34958  vonf1owevOLD  35465  deranglem  35529  derangsn  35533  derangenlem  35534  subfacp1lem4  35546  subfacp1lem5  35547  subfacp1lem6  35548  cvmfolem  35642  cvmliftlem6  35653  poimirlem1  38132  poimirlem2  38133  poimirlem3  38134  poimirlem4  38135  poimirlem6  38137  poimirlem7  38138  poimirlem9  38140  poimirlem11  38142  poimirlem12  38143  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  poimirlem22  38153  poimirlem26  38157  poimirlem27  38158  poimirlem28  38159  poimirlem32  38163  mblfinlem2  38169  dvasin  38215  f1ocan1fv  38237  metf1o  38266  ismtyval  38311  isismty  38312  ismtyima  38314  ismtyhmeolem  38315  ismtybndlem  38317  ismrer1  38349  reheibor  38350  grposnOLD  38393  rngoisocnv  38492  lflnegl  39712  lautset  40718  islaut  40719  lautcl  40723  lautco  40733  pautsetN  40734  ispautN  40735  ldilco  40752  ltrncoidN  40764  ltrncoval  40781  trlcoabs2N  41358  trlcoat  41359  trlcone  41364  cdlemg47a  41370  cdlemg46  41371  cdlemg47  41372  trljco  41376  tgrpgrplem  41385  tendoidcl  41405  tendo0co2  41424  tendo0pl  41427  cdlemi2  41455  cdlemk2  41468  cdlemk4  41470  cdlemk8  41474  cdlemkid2  41560  cdlemk45  41583  cdlemk53b  41592  cdlemk53  41593  cdlemk55a  41595  erng1r  41631  tendocnv  41657  dvalveclem  41661  dva0g  41663  dvhgrp  41743  dvh0g  41747  dvhopN  41752  cdlemn3  41833  cdlemn8  41840  cdlemn9  41841  dihordlem7b  41851  dihopelvalcpre  41884  dihmeetlem1N  41926  dihglblem5apreN  41927  lcfrlem13  42191  hvmapclN  42400  hvmapcl2  42402  dvrelog2  42693  dvrelog3  42694  sticksstones3  42777  sticksstones17  42792  sticksstones18  42793  sticksstones19  42794  readvrec2  42982  readvrec  42983  mapfzcons  43309  mzpresrename  43343  diophrw  43352  eldioph2  43355  diophren  43402  kelac1  43652  imasgim  43689  lnrfg  43708  nvocnvb  44010  brco2f1o  44620  brco3f1o  44621  clsneikex  44694  clsneinex  44695  clsneiel1  44696  neicvgmex  44705  neicvgel1  44707  dssmapntrcls  44716  stoweidlem27  46599  stoweidlem31  46603  stoweidlem39  46611  fourierdlem20  46699  fourierdlem50  46728  fourierdlem52  46730  fourierdlem54  46732  fourierdlem64  46742  fourierdlem76  46754  fourierdlem102  46780  fourierdlem114  46792  sge0f1o  46954  nnfoctbdjlem  47027  isomenndlem  47102  ovnsubaddlem1  47142  3f1oss1  47667  reuf1odnf  47699  reuf1od  47700  f1oresf1o2  47883  fundcmpsurbijinjpreimafv  48011  fundcmpsurinjimaid  48015  grimfn  48499  isgrim  48502  grimuhgr  48507  grimco  48509  uhgrimedgi  48510  isuspgrim0lem  48513  isuspgrim0  48514  isuspgrim  48516  upgrimwlklem4  48520  gricushgr  48537  isubgrgrim  48549  uhgrimisgrgriclem  48550  uhgrimisgrgric  48551  clnbgrgrim  48554  grimedg  48555  grtriclwlk3  48565  isubgr3stgrlem3  48588  isubgr3stgrlem4  48589  isubgr3stgrlem6  48591  isubgr3stgrlem7  48592  isubgr3stgrlem8  48593  isubgr3stgrlem9  48594  grlimfn  48599  isgrlim  48602  uspgrlimlem1  48608  uspgrlimlem2  48609  uspgrlimlem3  48610  uspgrlimlem4  48611  grlimprclnbgredg  48617  grlimgredgex  48620  grlimgrtrilem2  48622  grlictr  48635  clnbgr3stgrgrlim  48639  clnbgr3stgrgrlic  48640  1hegrlfgr  48752  funcringcsetcALTV2lem8  48917  funcringcsetclem8ALTV  48940  itcovalendof  49300  uptrlem1  49839  uptr2  49850  swapf2f1oaALT  49907  swapfcoa  49910  swapffunc  49911  fucoppc  50039  thincciso  50082  thinccisod  50083  lmdran  50300  cmdlan  50301  amgmwlem  50431