Theorem f1of 6802

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 6801	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
2		f1f 6756	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ⟶wf 6513  –1-1→wf1 6514  –1-1-onto→wf1o 6516

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 209  df-an 400  df-f1 6522  df-f1o 6524

This theorem is referenced by:  f1ofn  6803  f1ompt  7088  f1oresrab  7105  fsn  7113  fsnunf  7165  f1ounsn  7252  f1ocnvfv1  7256  f1ocnvfv2  7257  fsnex  7263  f1ocnvdm  7265  fcof1oinvd  7273  fveqf1o  7282  isocnv  7310  isocnv3  7312  isores2  7313  isotr  7316  isofr2  7324  isopolem  7325  isosolem  7327  f1oiso2  7332  weniso  7334  f1ofveu  7386  f1oexrnex  7904  f1oabexg  7918  wemoiso  7950  mptcnfimad  7963  suppsnop  8153  smoiso  8328  mapsnd  8864  ralxpmap  8874  f1oen2g  8945  en1  9001  enfixsn  9054  mapen  9109  ac6sfi  9224  domunfican  9262  fiint  9267  mapfienlem1  9348  mapfienlem2  9349  mapfienlem3  9350  mapfien  9351  supisoex  9418  supiso  9419  ordiso2  9460  unxpwdom2  9533  cantnfle  9623  cantnfp1lem3  9632  cantnflem1b  9638  cantnflem1d  9640  cantnflem1  9641  cnfcomlem  9651  cnfcom  9652  cnfcom2lem  9653  cnfcom2  9654  cnfcom3lem  9655  cnfcom3  9656  cnfcom3clem  9657  djuin  9873  infxpenlem  9966  infxpenc  9971  infxpenc2lem2  9973  fseqenlem1  9977  acndom  10004  acndom2  10007  infpwfien  10015  iunfictbso  10067  infmap2  10170  ackbij2lem2  10192  infpssrlem3  10259  infpssrlem4  10260  fin23lem30  10296  isf32lem6  10312  isf32lem7  10313  isf32lem8  10314  enfin1ai  10338  axcc3  10392  axcclem  10411  ttukeylem7  10469  fpwwe2lem5  10590  fpwwe2lem6  10591  fpwwe2lem8  10593  canthp1lem2  10608  canthp1  10609  pwfseqlem4a  10616  pwfseqlem5  10618  axdc4uzlem  13993  seqf1olem1  14051  seqf1olem2  14052  seqf1o  14053  hashkf  14342  hasheqf1oi  14361  hasheqf1od  14363  hashcl  14366  hashgadd  14387  hashfacen  14464  hashf1lem1  14465  fz1isolem  14471  seqcoll  14474  seqcoll2  14475  cnrecnv  15175  sumeq2ii  15703  summolem3  15724  summolem2a  15725  fsum  15730  fsumf1o  15733  fsumss  15735  fsumcl2lem  15741  fsumadd  15750  fsummulc2  15794  fsumrelem  15818  ackbijnn  15841  prodeq2ii  15924  prodmolem3  15946  prodmolem2a  15947  fprod  15954  fprodf1o  15959  fprodss  15961  fprodser  15962  fprodcl2lem  15963  fprodmul  15973  fproddiv  15974  fprodn0  15992  fproddvdsd  16352  sadcaddlem  16474  sadadd2lem  16476  sadadd3  16478  sadaddlem  16483  sadasslem  16487  sadeq  16489  phimullem  16797  eulerthlem1  16799  eulerthlem2  16800  unbenlem  16927  vdwlem8  17007  0ram  17039  wunndx  17214  xpsaddlem  17586  xpsvsca  17590  xpsle  17592  idfucl  17897  setccatid  18100  setcinv  18106  catcisolem  18126  estrccatid  18147  funcestrcsetclem7  18161  funcestrcsetclem8  18162  funcsetcestrclem7  18176  funcsetcestrclem8  18177  yonffthlem  18297  gsumpropd2lem  18696  mgmhmf1o  18717  idmgmhm  18718  idmhm  18812  mhmf1o  18813  gsumws1  18855  ielefmnd  18904  idghm  19254  ghmf1o  19271  symgbas  19395  elsymgbas  19397  symgbasf  19399  symgbasfi  19402  symg1bas  19414  symggrp  19423  lactghmga  19428  symgfixf1  19460  f1omvdmvd  19466  f1omvdconj  19469  f1omvdco2  19471  pmtrfconj  19489  symggen  19493  pmtrdifellem1  19499  pmtrdifellem2  19500  psgnunilem1  19516  gsumval3eu  19927  gsumval3lem1  19928  gsumval3  19930  gsumzf1o  19935  gsumconst  19957  gsumsub  19971  gsumcom2  19998  dprdfsub  20046  dprdf1o  20057  dprdsn  20061  ablfaclem2  20111  rngisomfv1  20493  rngisom1  20494  rngisomring1  20496  fidomndrnglem  20801  srngcl  20878  lmhmf1o  21093  gsumfsum  21466  zntoslem  21588  islinds2  21845  lindsmm  21860  psrass1lem  21965  psrnegcl  21986  psrlinv  21987  coe1f2  22251  coe1add  22307  evls1rhmlem  22364  evl1sca  22377  pf1ind  22398  mat1dimelbas  22511  mat1f  22522  mdetleib2  22628  mdetrsca  22643  mdetralt  22648  mdetunilem7  22658  mdetunilem9  22660  ssidcn  23295  hmphdis  23836  indishmph  23838  cmphaushmeo  23840  ordthmeolem  23841  txhmeo  23843  qtopf1  23856  ufldom  24002  symgtgp  24146  tsmsf1o  24185  iducn  24322  imasdsf1olem  24413  xpsdsval  24421  imasf1obl  24528  icchmeo  24983  iccpnfcnv  24986  xrhmeo  24988  cnheiborlem  24996  ovolctb  25532  ovoliunlem1  25544  ovoliunlem2  25545  iunmbl2  25599  dyadmbl  25642  vitalilem2  25651  vitalilem3  25652  vitalilem4  25653  vitalilem5  25654  mbfid  25677  dvid  25960  dvexp  25995  dvcnvlem  26018  dvcnv  26019  dvcnvrelem2  26060  dvcnvre  26061  efcvx  26489  reefgim  26490  efif1olem4  26587  eff1olem  26590  logrncl  26609  relogcl  26617  dvrelog  26679  relogcn  26680  logcn  26689  logf1o2  26692  dvlog  26693  dvlog2  26695  advlog  26696  advlogexp  26697  logtayl  26702  logccv  26705  dvcxp1  26782  loglesqrt  26803  asinrebnd  26943  dvatan  26977  efrlim  27011  amgmlem  27031  lgamcvg2  27096  wilthlem2  27110  wilthlem3  27111  sqff1o  27223  lgsqrlem4  27390  logdivsum  27574  log2sumbnd  27585  isismt  28680  motcl  28685  motco  28686  cnvmot  28687  motgrp  28689  motcgrg  28690  f1otrg  29017  f1otrge  29018  axlowdimlem10  29098  axcontlem5  29115  axcontlem10  29120  uspgriedgedg  29323  upgrres1  29460  umgrres1  29461  upgriseupth  30355  pliguhgr  30635  dmadjrn  32044  unopnorm  32066  unopadj  32068  unoplin  32069  counop  32070  idcnop  32130  idhmop  32131  unopbd  32164  bracnln  32258  cnvbraval  32259  leopnmid  32287  nmopleid  32288  hmopidmch  32302  hmopidmpj  32303  disjrdx  32740  fmptco1f1o  32785  isoun  32854  padct  32870  fcobij  32872  fcobijfs  32873  fcobijfs2  32874  wrdpmcl  33077  ccatws1f1o  33090  ccatws1f1olast  33091  mndlactf1o  33169  mndractf1o  33170  abliso  33175  symgfcoeu  33223  symgcom  33224  pmtrcnel  33230  pmtrcnel2  33231  pmtrcnelor  33232  wrdpmtrlast  33234  cycpmco2f1  33265  cycpmco2rn  33266  cycpmco2lem2  33268  cycpmco2lem3  33269  cycpmco2lem4  33270  cycpmco2lem5  33271  cycpmco2lem6  33272  cycpmco2lem7  33273  cycpmco2  33274  cycpmconjv  33283  cycpmconjslem1  33295  cycpmconjslem2  33296  cycpmconjs  33297  islinds5  33514  ellspds  33515  1arithidomlem1  33692  1arithidomlem2  33693  1arithidom  33694  0mplrim  33772  selvply1rhmlemb  33777  mplvrpmlem  33801  mplvrpmfgalem  33802  mplvrpmmhm  33804  mplvrpmrhm  33805  esplyfval0  33822  esplylem  33824  esplympl  33825  esplymhp  33826  esplyfv1  33827  esplyfv  33828  esplysply  33829  esplyfval3  33830  vieta  33838  tpr2rico  34170  xrge0iifmhm  34197  xrge0pluscn  34198  rrhre  34279  esumf1o  34308  volmeas  34489  eulerpartgbij  34630  eulerpartlemmf  34633  eulerpartlemgvv  34634  eulerpartlemgf  34637  eulerpartlemgs2  34638  eulerpartlemn  34639  ballotlemsima  34774  reprpmtf1o  34884  logdivsqrle  34908  hgt750lemg  34912  vonf1owevOLD  35417  deranglem  35480  derangsn  35484  derangenlem  35485  subfacp1lem4  35497  subfacp1lem5  35498  subfacp1lem6  35499  cvmfolem  35593  cvmliftlem6  35604  poimirlem1  38084  poimirlem2  38085  poimirlem3  38086  poimirlem4  38087  poimirlem6  38089  poimirlem7  38090  poimirlem9  38092  poimirlem11  38094  poimirlem12  38095  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  poimirlem22  38105  poimirlem26  38109  poimirlem27  38110  poimirlem28  38111  poimirlem32  38115  mblfinlem2  38121  dvasin  38167  f1ocan1fv  38189  metf1o  38218  ismtyval  38263  isismty  38264  ismtyima  38266  ismtyhmeolem  38267  ismtybndlem  38269  ismrer1  38301  reheibor  38302  grposnOLD  38345  rngoisocnv  38444  lflnegl  39664  lautset  40670  islaut  40671  lautcl  40675  lautco  40685  pautsetN  40686  ispautN  40687  ldilco  40704  ltrncoidN  40716  ltrncoval  40733  trlcoabs2N  41310  trlcoat  41311  trlcone  41316  cdlemg47a  41322  cdlemg46  41323  cdlemg47  41324  trljco  41328  tgrpgrplem  41337  tendoidcl  41357  tendo0co2  41376  tendo0pl  41379  cdlemi2  41407  cdlemk2  41420  cdlemk4  41422  cdlemk8  41426  cdlemkid2  41512  cdlemk45  41535  cdlemk53b  41544  cdlemk53  41545  cdlemk55a  41547  erng1r  41583  tendocnv  41609  dvalveclem  41613  dva0g  41615  dvhgrp  41695  dvh0g  41699  dvhopN  41704  cdlemn3  41785  cdlemn8  41792  cdlemn9  41793  dihordlem7b  41803  dihopelvalcpre  41836  dihmeetlem1N  41878  dihglblem5apreN  41879  lcfrlem13  42143  hvmapclN  42352  hvmapcl2  42354  dvrelog2  42645  dvrelog3  42646  sticksstones3  42729  sticksstones17  42744  sticksstones18  42745  sticksstones19  42746  readvrec2  42934  readvrec  42935  mapfzcons  43261  mzpresrename  43295  diophrw  43304  eldioph2  43307  diophren  43354  kelac1  43604  imasgim  43641  lnrfg  43660  nvocnvb  43962  brco2f1o  44572  brco3f1o  44573  clsneikex  44646  clsneinex  44647  clsneiel1  44648  neicvgmex  44657  neicvgel1  44659  dssmapntrcls  44668  stoweidlem27  46565  stoweidlem31  46569  stoweidlem39  46577  fourierdlem20  46665  fourierdlem50  46694  fourierdlem52  46696  fourierdlem54  46698  fourierdlem64  46708  fourierdlem76  46720  fourierdlem102  46746  fourierdlem114  46758  sge0f1o  46920  nnfoctbdjlem  46993  isomenndlem  47068  ovnsubaddlem1  47108  3f1oss1  47633  reuf1odnf  47665  reuf1od  47666  f1oresf1o2  47849  fundcmpsurbijinjpreimafv  47977  fundcmpsurinjimaid  47981  grimfn  48465  isgrim  48468  grimuhgr  48473  grimco  48475  uhgrimedgi  48476  isuspgrim0lem  48479  isuspgrim0  48480  isuspgrim  48482  upgrimwlklem4  48486  gricushgr  48503  isubgrgrim  48515  uhgrimisgrgriclem  48516  uhgrimisgrgric  48517  clnbgrgrim  48520  grimedg  48521  grtriclwlk3  48531  isubgr3stgrlem3  48554  isubgr3stgrlem4  48555  isubgr3stgrlem6  48557  isubgr3stgrlem7  48558  isubgr3stgrlem8  48559  isubgr3stgrlem9  48560  grlimfn  48565  isgrlim  48568  uspgrlimlem1  48574  uspgrlimlem2  48575  uspgrlimlem3  48576  uspgrlimlem4  48577  grlimprclnbgredg  48583  grlimgredgex  48586  grlimgrtrilem2  48588  grlictr  48601  clnbgr3stgrgrlim  48605  clnbgr3stgrgrlic  48606  1hegrlfgr  48718  funcringcsetcALTV2lem8  48883  funcringcsetclem8ALTV  48906  itcovalendof  49255  uptrlem1  49795  uptr2  49806  swapf2f1oaALT  49863  swapfcoa  49866  swapffunc  49867  fucoppc  49995  thincciso  50038  thinccisod  50039  lmdran  50256  cmdlan  50257  amgmwlem  50387