Theorem f1of 6763

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

Syntax hints:   → wi 4  ⟶wf 6477  –1-1→wf1 6478  –1-1-onto→wf1o 6480

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 6486  df-f1o 6488

This theorem is referenced by:  f1ofn  6764  f1ompt  7044  f1oresrab  7060  fsn  7068  fsnunf  7119  f1ounsn  7206  f1ocnvfv1  7210  f1ocnvfv2  7211  fsnex  7217  f1ocnvdm  7219  fcof1oinvd  7227  fveqf1o  7236  isocnv  7264  isocnv3  7266  isores2  7267  isotr  7270  isofr2  7278  isopolem  7279  isosolem  7281  f1oiso2  7286  weniso  7288  f1ofveu  7340  f1oexrnex  7857  f1oabexg  7872  f1oabexgOLD  7873  wemoiso  7905  mptcnfimad  7918  suppsnop  8108  smoiso  8282  mapsnd  8810  ralxpmap  8820  f1oen2g  8891  en1  8946  enfixsn  8999  mapen  9054  ac6sfi  9168  domunfican  9206  fiint  9211  mapfienlem1  9289  mapfienlem2  9290  mapfienlem3  9291  mapfien  9292  supisoex  9359  supiso  9360  ordiso2  9401  unxpwdom2  9474  cantnfle  9561  cantnfp1lem3  9570  cantnflem1b  9576  cantnflem1d  9578  cantnflem1  9579  cnfcomlem  9589  cnfcom  9590  cnfcom2lem  9591  cnfcom2  9592  cnfcom3lem  9593  cnfcom3  9594  cnfcom3clem  9595  djuin  9811  infxpenlem  9904  infxpenc  9909  infxpenc2lem2  9911  fseqenlem1  9915  acndom  9942  acndom2  9945  infpwfien  9953  iunfictbso  10005  infmap2  10108  ackbij2lem2  10130  infpssrlem3  10196  infpssrlem4  10197  fin23lem30  10233  isf32lem6  10249  isf32lem7  10250  isf32lem8  10251  enfin1ai  10275  axcc3  10329  axcclem  10348  ttukeylem7  10406  fpwwe2lem5  10526  fpwwe2lem6  10527  fpwwe2lem8  10529  canthp1lem2  10544  canthp1  10545  pwfseqlem4a  10552  pwfseqlem5  10554  axdc4uzlem  13890  seqf1olem1  13948  seqf1olem2  13949  seqf1o  13950  hashkf  14239  hasheqf1oi  14258  hasheqf1od  14260  hashcl  14263  hashgadd  14284  hashfacen  14361  hashf1lem1  14362  fz1isolem  14368  seqcoll  14371  seqcoll2  14372  cnrecnv  15072  sumeq2ii  15600  summolem3  15621  summolem2a  15622  fsum  15627  fsumf1o  15630  fsumss  15632  fsumcl2lem  15638  fsumadd  15647  fsummulc2  15691  fsumrelem  15714  ackbijnn  15735  prodeq2ii  15818  prodmolem3  15840  prodmolem2a  15841  fprod  15848  fprodf1o  15853  fprodss  15855  fprodser  15856  fprodcl2lem  15857  fprodmul  15867  fproddiv  15868  fprodn0  15886  fproddvdsd  16246  sadcaddlem  16368  sadadd2lem  16370  sadadd3  16372  sadaddlem  16377  sadasslem  16381  sadeq  16383  phimullem  16690  eulerthlem1  16692  eulerthlem2  16693  unbenlem  16820  vdwlem8  16900  0ram  16932  wunndx  17106  xpsaddlem  17477  xpsvsca  17481  xpsle  17483  idfucl  17788  setccatid  17991  setcinv  17997  catcisolem  18017  estrccatid  18038  funcestrcsetclem7  18052  funcestrcsetclem8  18053  funcsetcestrclem7  18067  funcsetcestrclem8  18068  yonffthlem  18188  gsumpropd2lem  18587  mgmhmf1o  18608  idmgmhm  18609  idmhm  18703  mhmf1o  18704  gsumws1  18746  ielefmnd  18795  idghm  19143  ghmf1o  19160  symgbas  19284  elsymgbas  19286  symgbasf  19288  symgbasfi  19291  symg1bas  19303  symggrp  19312  lactghmga  19317  symgfixf1  19349  f1omvdmvd  19355  f1omvdconj  19358  f1omvdco2  19360  pmtrfconj  19378  symggen  19382  pmtrdifellem1  19388  pmtrdifellem2  19389  psgnunilem1  19405  gsumval3eu  19816  gsumval3lem1  19817  gsumval3  19819  gsumzf1o  19824  gsumconst  19846  gsumsub  19860  gsumcom2  19887  dprdfsub  19935  dprdf1o  19946  dprdsn  19950  ablfaclem2  20000  rngisomfv1  20383  rngisom1  20384  rngisomring1  20386  fidomndrnglem  20687  srngcl  20764  lmhmf1o  20980  gsumfsum  21371  zntoslem  21493  islinds2  21750  lindsmm  21765  psrass1lem  21869  psrnegcl  21891  psrlinv  21892  coe1f2  22122  coe1add  22178  evls1rhmlem  22236  evl1sca  22249  pf1ind  22270  mat1dimelbas  22386  mat1f  22397  mdetleib2  22503  mdetrsca  22518  mdetralt  22523  mdetunilem7  22533  mdetunilem9  22535  ssidcn  23170  hmphdis  23711  indishmph  23713  cmphaushmeo  23715  ordthmeolem  23716  txhmeo  23718  qtopf1  23731  ufldom  23877  symgtgp  24021  tsmsf1o  24060  iducn  24197  imasdsf1olem  24288  xpsdsval  24296  imasf1obl  24403  icchmeo  24865  icchmeoOLD  24866  iccpnfcnv  24869  xrhmeo  24871  cnheiborlem  24880  ovolctb  25418  ovoliunlem1  25430  ovoliunlem2  25431  iunmbl2  25485  dyadmbl  25528  vitalilem2  25537  vitalilem3  25538  vitalilem4  25539  vitalilem5  25540  mbfid  25563  dvid  25846  dvexp  25884  dvcnvlem  25907  dvcnv  25908  dvcnvrelem2  25950  dvcnvre  25951  efcvx  26386  reefgim  26387  efif1olem4  26481  eff1olem  26484  logrncl  26503  relogcl  26511  dvrelog  26573  relogcn  26574  logcn  26583  logf1o2  26586  dvlog  26587  dvlog2  26589  advlog  26590  advlogexp  26591  logtayl  26596  logccv  26599  dvcxp1  26676  loglesqrt  26698  asinrebnd  26838  dvatan  26872  efrlim  26906  efrlimOLD  26907  amgmlem  26927  lgamcvg2  26992  wilthlem2  27006  wilthlem3  27007  sqff1o  27119  lgsqrlem4  27287  logdivsum  27471  log2sumbnd  27482  isismt  28512  motcl  28517  motco  28518  cnvmot  28519  motgrp  28521  motcgrg  28522  f1otrg  28849  f1otrge  28850  axlowdimlem10  28929  axcontlem5  28946  axcontlem10  28951  uspgriedgedg  29154  upgrres1  29291  umgrres1  29292  upgriseupth  30187  pliguhgr  30466  dmadjrn  31875  unopnorm  31897  unopadj  31899  unoplin  31900  counop  31901  idcnop  31961  idhmop  31962  unopbd  31995  bracnln  32089  cnvbraval  32090  leopnmid  32118  nmopleid  32119  hmopidmch  32133  hmopidmpj  32134  disjrdx  32571  fmptco1f1o  32615  isoun  32683  padct  32701  fcobij  32703  fcobijfs  32704  fcobijfs2  32705  wrdpmcl  32919  ccatws1f1o  32932  ccatws1f1olast  32933  mndlactf1o  33011  mndractf1o  33012  abliso  33017  symgfcoeu  33051  symgcom  33052  pmtrcnel  33058  pmtrcnel2  33059  pmtrcnelor  33060  wrdpmtrlast  33062  cycpmco2f1  33093  cycpmco2rn  33094  cycpmco2lem2  33096  cycpmco2lem3  33097  cycpmco2lem4  33098  cycpmco2lem5  33099  cycpmco2lem6  33100  cycpmco2lem7  33101  cycpmco2  33102  cycpmconjv  33111  cycpmconjslem1  33123  cycpmconjslem2  33124  cycpmconjs  33125  islinds5  33332  ellspds  33333  1arithidomlem1  33500  1arithidomlem2  33501  1arithidom  33502  mplvrpmlem  33573  mplvrpmfgalem  33574  mplvrpmmhm  33576  mplvrpmrhm  33577  esplylem  33587  esplympl  33588  esplymhp  33589  esplyfv1  33590  esplyfv  33591  esplysply  33592  tpr2rico  33925  xrge0iifmhm  33952  xrge0pluscn  33953  rrhre  34034  esumf1o  34063  volmeas  34244  eulerpartgbij  34385  eulerpartlemmf  34388  eulerpartlemgvv  34389  eulerpartlemgf  34392  eulerpartlemgs2  34393  eulerpartlemn  34394  ballotlemsima  34529  reprpmtf1o  34639  logdivsqrle  34663  hgt750lemg  34667  vonf1owev  35152  deranglem  35210  derangsn  35214  derangenlem  35215  subfacp1lem4  35227  subfacp1lem5  35228  subfacp1lem6  35229  cvmfolem  35323  cvmliftlem6  35334  poimirlem1  37660  poimirlem2  37661  poimirlem3  37662  poimirlem4  37663  poimirlem6  37665  poimirlem7  37666  poimirlem9  37668  poimirlem11  37670  poimirlem12  37671  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem22  37681  poimirlem26  37685  poimirlem27  37686  poimirlem28  37687  poimirlem32  37691  mblfinlem2  37697  dvasin  37743  f1ocan1fv  37765  metf1o  37794  ismtyval  37839  isismty  37840  ismtyima  37842  ismtyhmeolem  37843  ismtybndlem  37845  ismrer1  37877  reheibor  37878  grposnOLD  37921  rngoisocnv  38020  lflnegl  39174  lautset  40180  islaut  40181  lautcl  40185  lautco  40195  pautsetN  40196  ispautN  40197  ldilco  40214  ltrncoidN  40226  ltrncoval  40243  trlcoabs2N  40820  trlcoat  40821  trlcone  40826  cdlemg47a  40832  cdlemg46  40833  cdlemg47  40834  trljco  40838  tgrpgrplem  40847  tendoidcl  40867  tendo0co2  40886  tendo0pl  40889  cdlemi2  40917  cdlemk2  40930  cdlemk4  40932  cdlemk8  40936  cdlemkid2  41022  cdlemk45  41045  cdlemk53b  41054  cdlemk53  41055  cdlemk55a  41057  erng1r  41093  tendocnv  41119  dvalveclem  41123  dva0g  41125  dvhgrp  41205  dvh0g  41209  dvhopN  41214  cdlemn3  41295  cdlemn8  41302  cdlemn9  41303  dihordlem7b  41313  dihopelvalcpre  41346  dihmeetlem1N  41388  dihglblem5apreN  41389  lcfrlem13  41653  hvmapclN  41862  hvmapcl2  41864  dvrelog2  42156  dvrelog3  42157  sticksstones3  42240  sticksstones17  42255  sticksstones18  42256  sticksstones19  42257  readvrec2  42453  readvrec  42454  mapfzcons  42808  mzpresrename  42842  diophrw  42851  eldioph2  42854  diophren  42905  kelac1  43155  imasgim  43192  lnrfg  43211  nvocnvb  43514  brco2f1o  44124  brco3f1o  44125  clsneikex  44198  clsneinex  44199  clsneiel1  44200  neicvgmex  44209  neicvgel1  44211  dssmapntrcls  44220  stoweidlem27  46124  stoweidlem31  46128  stoweidlem39  46136  fourierdlem20  46224  fourierdlem50  46253  fourierdlem52  46255  fourierdlem54  46257  fourierdlem64  46267  fourierdlem76  46279  fourierdlem102  46305  fourierdlem114  46317  sge0f1o  46479  nnfoctbdjlem  46552  isomenndlem  46627  ovnsubaddlem1  46667  3f1oss1  47174  reuf1odnf  47206  reuf1od  47207  f1oresf1o2  47390  fundcmpsurbijinjpreimafv  47506  fundcmpsurinjimaid  47510  grimfn  47978  isgrim  47981  grimuhgr  47986  grimco  47988  uhgrimedgi  47989  isuspgrim0lem  47992  isuspgrim0  47993  isuspgrim  47995  upgrimwlklem4  47999  gricushgr  48016  isubgrgrim  48028  uhgrimisgrgriclem  48029  uhgrimisgrgric  48030  clnbgrgrim  48033  grimedg  48034  grtriclwlk3  48044  isubgr3stgrlem3  48067  isubgr3stgrlem4  48068  isubgr3stgrlem6  48070  isubgr3stgrlem7  48071  isubgr3stgrlem8  48072  isubgr3stgrlem9  48073  grlimfn  48078  isgrlim  48081  uspgrlimlem1  48087  uspgrlimlem2  48088  uspgrlimlem3  48089  uspgrlimlem4  48090  grlimprclnbgredg  48096  grlimgredgex  48099  grlimgrtrilem2  48101  grlictr  48114  clnbgr3stgrgrlim  48118  clnbgr3stgrgrlic  48119  1hegrlfgr  48231  funcringcsetcALTV2lem8  48396  funcringcsetclem8ALTV  48419  itcovalendof  48769  uptrlem1  49310  uptr2  49321  swapf2f1oaALT  49378  swapfcoa  49381  swapffunc  49382  fucoppc  49510  thincciso  49553  thinccisod  49554  lmdran  49771  cmdlan  49772  amgmwlem  49902