Theorem f1of 6846

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

Syntax hints:   → wi 4  ⟶wf 6555  –1-1→wf1 6556  –1-1-onto→wf1o 6558

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 207  df-an 396  df-f1 6564  df-f1o 6566

This theorem is referenced by:  f1ofn  6847  f1ompt  7129  f1oresrab  7145  fsn  7153  fsnunf  7203  f1ounsn  7290  f1ocnvfv1  7294  f1ocnvfv2  7295  fsnex  7301  f1ocnvdm  7303  fcof1oinvd  7311  fveqf1o  7320  isocnv  7348  isocnv3  7350  isores2  7351  isotr  7354  isofr2  7362  isopolem  7363  isosolem  7365  f1oiso2  7370  weniso  7372  f1ofveu  7423  f1oexrnex  7945  f1oabexg  7960  f1oabexgOLD  7961  wemoiso  7994  mptcnfimad  8007  suppsnop  8199  smoiso  8398  mapsnd  8922  ralxpmap  8932  f1oen2g  9005  en1  9060  enfixsn  9117  mapen  9177  ac6sfi  9316  domunfican  9357  fiint  9362  fiintOLD  9363  mapfienlem1  9441  mapfienlem2  9442  mapfienlem3  9443  mapfien  9444  supisoex  9510  supiso  9511  ordiso2  9551  unxpwdom2  9624  cantnfle  9707  cantnfp1lem3  9716  cantnflem1b  9722  cantnflem1d  9724  cantnflem1  9725  cnfcomlem  9735  cnfcom  9736  cnfcom2lem  9737  cnfcom2  9738  cnfcom3lem  9739  cnfcom3  9740  cnfcom3clem  9741  djuin  9954  infxpenlem  10049  infxpenc  10054  infxpenc2lem2  10056  fseqenlem1  10060  acndom  10087  acndom2  10090  infpwfien  10098  iunfictbso  10150  infmap2  10253  ackbij2lem2  10275  infpssrlem3  10341  infpssrlem4  10342  fin23lem30  10378  isf32lem6  10394  isf32lem7  10395  isf32lem8  10396  enfin1ai  10420  axcc3  10474  axcclem  10493  ttukeylem7  10551  fpwwe2lem5  10671  fpwwe2lem6  10672  fpwwe2lem8  10674  canthp1lem2  10689  canthp1  10690  pwfseqlem4a  10697  pwfseqlem5  10699  axdc4uzlem  14020  seqf1olem1  14078  seqf1olem2  14079  seqf1o  14080  hashkf  14367  hasheqf1oi  14386  hasheqf1od  14388  hashcl  14391  hashgadd  14412  hashfacen  14489  hashf1lem1  14490  fz1isolem  14496  seqcoll  14499  seqcoll2  14500  cnrecnv  15200  sumeq2ii  15725  summolem3  15746  summolem2a  15747  fsum  15752  fsumf1o  15755  fsumss  15757  fsumcl2lem  15763  fsumadd  15772  fsummulc2  15816  fsumrelem  15839  ackbijnn  15860  prodeq2ii  15943  prodmolem3  15965  prodmolem2a  15966  fprod  15973  fprodf1o  15978  fprodss  15980  fprodser  15981  fprodcl2lem  15982  fprodmul  15992  fproddiv  15993  fprodn0  16011  fproddvdsd  16368  sadcaddlem  16490  sadadd2lem  16492  sadadd3  16494  sadaddlem  16499  sadasslem  16503  sadeq  16505  phimullem  16812  eulerthlem1  16814  eulerthlem2  16815  unbenlem  16942  vdwlem8  17022  0ram  17054  wunndx  17228  xpsaddlem  17614  xpsvsca  17618  xpsle  17620  idfucl  17922  setccatid  18125  setcinv  18131  catcisolem  18151  estrccatid  18172  funcestrcsetclem7  18187  funcestrcsetclem8  18188  funcsetcestrclem7  18202  funcsetcestrclem8  18203  yonffthlem  18323  gsumpropd2lem  18688  mgmhmf1o  18709  idmgmhm  18710  idmhm  18804  mhmf1o  18805  gsumws1  18847  ielefmnd  18896  idghm  19245  ghmf1o  19262  symgbas  19385  elsymgbas  19387  symgbasf  19389  symgbasfi  19392  symg1bas  19404  symggrp  19414  lactghmga  19419  symgfixf1  19451  f1omvdmvd  19457  f1omvdconj  19460  f1omvdco2  19462  pmtrfconj  19480  symggen  19484  pmtrdifellem1  19490  pmtrdifellem2  19491  psgnunilem1  19507  gsumval3eu  19918  gsumval3lem1  19919  gsumval3  19921  gsumzf1o  19926  gsumconst  19948  gsumsub  19962  gsumcom2  19989  dprdfsub  20037  dprdf1o  20048  dprdsn  20052  ablfaclem2  20102  rngisomfv1  20457  rngisom1  20458  rngisomring1  20460  fidomndrnglem  20765  srngcl  20842  lmhmf1o  21037  gsumfsum  21444  zntoslem  21567  islinds2  21825  lindsmm  21840  psrass1lem  21944  psrnegcl  21966  psrlinv  21967  coe1f2  22201  coe1add  22257  evls1rhmlem  22315  evl1sca  22328  pf1ind  22349  mat1dimelbas  22467  mat1f  22478  mdetleib2  22584  mdetrsca  22599  mdetralt  22604  mdetunilem7  22614  mdetunilem9  22616  ssidcn  23253  hmphdis  23794  indishmph  23796  cmphaushmeo  23798  ordthmeolem  23799  txhmeo  23801  qtopf1  23814  ufldom  23960  symgtgp  24104  tsmsf1o  24143  iducn  24282  imasdsf1olem  24373  xpsdsval  24381  imasf1obl  24491  icchmeo  24961  icchmeoOLD  24962  iccpnfcnv  24965  xrhmeo  24967  cnheiborlem  24976  ovolctb  25515  ovoliunlem1  25527  ovoliunlem2  25528  iunmbl2  25582  dyadmbl  25625  vitalilem2  25634  vitalilem3  25635  vitalilem4  25636  vitalilem5  25637  mbfid  25660  dvid  25943  dvexp  25981  dvcnvlem  26004  dvcnv  26005  dvcnvrelem2  26047  dvcnvre  26048  efcvx  26483  reefgim  26484  efif1olem4  26577  eff1olem  26580  logrncl  26599  relogcl  26607  dvrelog  26669  relogcn  26670  logcn  26679  logf1o2  26682  dvlog  26683  dvlog2  26685  advlog  26686  advlogexp  26687  logtayl  26692  logccv  26695  dvcxp1  26772  loglesqrt  26794  asinrebnd  26934  dvatan  26968  efrlim  27002  efrlimOLD  27003  amgmlem  27023  lgamcvg2  27088  wilthlem2  27102  wilthlem3  27103  sqff1o  27215  lgsqrlem4  27383  logdivsum  27567  log2sumbnd  27578  isismt  28532  motcl  28537  motco  28538  cnvmot  28539  motgrp  28541  motcgrg  28542  f1otrg  28869  f1otrge  28870  axlowdimlem10  28956  axcontlem5  28973  axcontlem10  28978  uspgriedgedg  29183  upgrres1  29320  umgrres1  29321  upgriseupth  30216  pliguhgr  30495  dmadjrn  31904  unopnorm  31926  unopadj  31928  unoplin  31929  counop  31930  idcnop  31990  idhmop  31991  unopbd  32024  bracnln  32118  cnvbraval  32119  leopnmid  32147  nmopleid  32148  hmopidmch  32162  hmopidmpj  32163  disjrdx  32593  fmptco1f1o  32632  isoun  32700  padct  32720  fcobij  32722  fcobijfs  32723  wrdpmcl  32909  ccatws1f1o  32923  ccatws1f1olast  32924  mndlactf1o  33020  mndractf1o  33021  abliso  33026  symgfcoeu  33087  symgcom  33088  pmtrcnel  33094  pmtrcnel2  33095  pmtrcnelor  33096  wrdpmtrlast  33098  cycpmco2f1  33129  cycpmco2rn  33130  cycpmco2lem2  33132  cycpmco2lem3  33133  cycpmco2lem4  33134  cycpmco2lem5  33135  cycpmco2lem6  33136  cycpmco2lem7  33137  cycpmco2  33138  cycpmconjv  33147  cycpmconjslem1  33159  cycpmconjslem2  33160  cycpmconjs  33161  islinds5  33382  ellspds  33383  1arithidomlem1  33550  1arithidomlem2  33551  1arithidom  33552  tpr2rico  33889  xrge0iifmhm  33916  xrge0pluscn  33917  rrhre  34000  esumf1o  34029  volmeas  34210  eulerpartgbij  34352  eulerpartlemmf  34355  eulerpartlemgvv  34356  eulerpartlemgf  34359  eulerpartlemgs2  34360  eulerpartlemn  34361  ballotlemsima  34496  reprpmtf1o  34619  logdivsqrle  34643  hgt750lemg  34647  deranglem  35149  derangsn  35153  derangenlem  35154  subfacp1lem4  35166  subfacp1lem5  35167  subfacp1lem6  35168  cvmfolem  35262  cvmliftlem6  35273  poimirlem1  37606  poimirlem2  37607  poimirlem3  37608  poimirlem4  37609  poimirlem6  37611  poimirlem7  37612  poimirlem9  37614  poimirlem11  37616  poimirlem12  37617  poimirlem16  37621  poimirlem17  37622  poimirlem19  37624  poimirlem20  37625  poimirlem22  37627  poimirlem26  37631  poimirlem27  37632  poimirlem28  37633  poimirlem32  37637  mblfinlem2  37643  dvasin  37689  f1ocan1fv  37711  metf1o  37740  ismtyval  37785  isismty  37786  ismtyima  37788  ismtyhmeolem  37789  ismtybndlem  37791  ismrer1  37823  reheibor  37824  grposnOLD  37867  rngoisocnv  37966  lflnegl  39055  lautset  40062  islaut  40063  lautcl  40067  lautco  40077  pautsetN  40078  ispautN  40079  ldilco  40096  ltrncoidN  40108  ltrncoval  40125  trlcoabs2N  40702  trlcoat  40703  trlcone  40708  cdlemg47a  40714  cdlemg46  40715  cdlemg47  40716  trljco  40720  tgrpgrplem  40729  tendoidcl  40749  tendo0co2  40768  tendo0pl  40771  cdlemi2  40799  cdlemk2  40812  cdlemk4  40814  cdlemk8  40818  cdlemkid2  40904  cdlemk45  40927  cdlemk53b  40936  cdlemk53  40937  cdlemk55a  40939  erng1r  40975  tendocnv  41001  dvalveclem  41005  dva0g  41007  dvhgrp  41087  dvh0g  41091  dvhopN  41096  cdlemn3  41177  cdlemn8  41184  cdlemn9  41185  dihordlem7b  41195  dihopelvalcpre  41228  dihmeetlem1N  41270  dihglblem5apreN  41271  lcfrlem13  41535  hvmapclN  41744  hvmapcl2  41746  dvrelog2  42043  dvrelog3  42044  sticksstones3  42127  sticksstones17  42142  sticksstones18  42143  sticksstones19  42144  metakunt33  42216  readvrec2  42369  readvrec  42370  mapfzcons  42705  mzpresrename  42739  diophrw  42748  eldioph2  42751  diophren  42802  kelac1  43053  imasgim  43090  lnrfg  43109  nvocnvb  43413  brco2f1o  44023  brco3f1o  44024  clsneikex  44097  clsneinex  44098  clsneiel1  44099  neicvgmex  44108  neicvgel1  44110  dssmapntrcls  44119  stoweidlem27  46015  stoweidlem31  46019  stoweidlem39  46027  fourierdlem20  46115  fourierdlem50  46144  fourierdlem52  46146  fourierdlem54  46148  fourierdlem64  46158  fourierdlem76  46170  fourierdlem102  46196  fourierdlem114  46208  sge0f1o  46370  nnfoctbdjlem  46443  isomenndlem  46518  ovnsubaddlem1  46558  3f1oss1  47060  reuf1odnf  47092  reuf1od  47093  f1oresf1o2  47276  fundcmpsurbijinjpreimafv  47367  fundcmpsurinjimaid  47371  grimfn  47838  isgrim  47841  isuspgrim0lem  47844  isuspgrim0  47845  uspgrimprop  47846  isuspgrim  47848  grimuhgr  47851  grimco  47853  gricushgr  47859  isubgrgrim  47870  uhgrimisgrgriclem  47871  uhgrimisgrgric  47872  clnbgrgrim  47875  grimedg  47876  grtriclwlk3  47885  isubgr3stgrlem3  47908  isubgr3stgrlem4  47909  isubgr3stgrlem6  47911  isubgr3stgrlem7  47912  isubgr3stgrlem8  47913  isubgr3stgrlem9  47914  grlimfn  47919  isgrlim  47922  uspgrlimlem1  47928  uspgrlimlem2  47929  uspgrlimlem3  47930  uspgrlimlem4  47931  grlimgrtrilem2  47935  grlictr  47948  clnbgr3stgrgrlic  47952  1hegrlfgr  48021  funcringcsetcALTV2lem8  48186  funcringcsetclem8ALTV  48209  itcovalendof  48563  swapf2f1oaALT  48957  swapfcoa  48960  swapffunc  48961  thincciso  49075  thinccisod  49076  amgmwlem  49294