Theorem f1of 6780

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

Syntax hints:   → wi 4  ⟶wf 6494  –1-1→wf1 6495  –1-1-onto→wf1o 6497

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 6503  df-f1o 6505

This theorem is referenced by:  f1ofn  6781  f1ompt  7063  f1oresrab  7080  fsn  7088  fsnunf  7140  f1ounsn  7227  f1ocnvfv1  7231  f1ocnvfv2  7232  fsnex  7238  f1ocnvdm  7240  fcof1oinvd  7248  fveqf1o  7257  isocnv  7285  isocnv3  7287  isores2  7288  isotr  7291  isofr2  7299  isopolem  7300  isosolem  7302  f1oiso2  7307  weniso  7309  f1ofveu  7361  f1oexrnex  7878  f1oabexg  7893  f1oabexgOLD  7894  wemoiso  7926  mptcnfimad  7939  suppsnop  8128  smoiso  8302  mapsnd  8834  ralxpmap  8844  f1oen2g  8915  en1  8971  enfixsn  9024  mapen  9079  ac6sfi  9194  domunfican  9232  fiint  9237  mapfienlem1  9318  mapfienlem2  9319  mapfienlem3  9320  mapfien  9321  supisoex  9388  supiso  9389  ordiso2  9430  unxpwdom2  9503  cantnfle  9592  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1d  9609  cantnflem1  9610  cnfcomlem  9620  cnfcom  9621  cnfcom2lem  9622  cnfcom2  9623  cnfcom3lem  9624  cnfcom3  9625  cnfcom3clem  9626  djuin  9842  infxpenlem  9935  infxpenc  9940  infxpenc2lem2  9942  fseqenlem1  9946  acndom  9973  acndom2  9976  infpwfien  9984  iunfictbso  10036  infmap2  10139  ackbij2lem2  10161  infpssrlem3  10227  infpssrlem4  10228  fin23lem30  10264  isf32lem6  10280  isf32lem7  10281  isf32lem8  10282  enfin1ai  10306  axcc3  10360  axcclem  10379  ttukeylem7  10437  fpwwe2lem5  10558  fpwwe2lem6  10559  fpwwe2lem8  10561  canthp1lem2  10576  canthp1  10577  pwfseqlem4a  10584  pwfseqlem5  10586  axdc4uzlem  13945  seqf1olem1  14003  seqf1olem2  14004  seqf1o  14005  hashkf  14294  hasheqf1oi  14313  hasheqf1od  14315  hashcl  14318  hashgadd  14339  hashfacen  14416  hashf1lem1  14417  fz1isolem  14423  seqcoll  14426  seqcoll2  14427  cnrecnv  15127  sumeq2ii  15655  summolem3  15676  summolem2a  15677  fsum  15682  fsumf1o  15685  fsumss  15687  fsumcl2lem  15693  fsumadd  15702  fsummulc2  15746  fsumrelem  15770  ackbijnn  15793  prodeq2ii  15876  prodmolem3  15898  prodmolem2a  15899  fprod  15906  fprodf1o  15911  fprodss  15913  fprodser  15914  fprodcl2lem  15915  fprodmul  15925  fproddiv  15926  fprodn0  15944  fproddvdsd  16304  sadcaddlem  16426  sadadd2lem  16428  sadadd3  16430  sadaddlem  16435  sadasslem  16439  sadeq  16441  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  unbenlem  16879  vdwlem8  16959  0ram  16991  wunndx  17165  xpsaddlem  17537  xpsvsca  17541  xpsle  17543  idfucl  17848  setccatid  18051  setcinv  18057  catcisolem  18077  estrccatid  18098  funcestrcsetclem7  18112  funcestrcsetclem8  18113  funcsetcestrclem7  18127  funcsetcestrclem8  18128  yonffthlem  18248  gsumpropd2lem  18647  mgmhmf1o  18668  idmgmhm  18669  idmhm  18763  mhmf1o  18764  gsumws1  18806  ielefmnd  18855  idghm  19206  ghmf1o  19223  symgbas  19347  elsymgbas  19349  symgbasf  19351  symgbasfi  19354  symg1bas  19366  symggrp  19375  lactghmga  19380  symgfixf1  19412  f1omvdmvd  19418  f1omvdconj  19421  f1omvdco2  19423  pmtrfconj  19441  symggen  19445  pmtrdifellem1  19451  pmtrdifellem2  19452  psgnunilem1  19468  gsumval3eu  19879  gsumval3lem1  19880  gsumval3  19882  gsumzf1o  19887  gsumconst  19909  gsumsub  19923  gsumcom2  19950  dprdfsub  19998  dprdf1o  20009  dprdsn  20013  ablfaclem2  20063  rngisomfv1  20445  rngisom1  20446  rngisomring1  20448  fidomndrnglem  20749  srngcl  20826  lmhmf1o  21041  gsumfsum  21414  zntoslem  21536  islinds2  21793  lindsmm  21808  psrass1lem  21912  psrnegcl  21933  psrlinv  21934  coe1f2  22173  coe1add  22229  evls1rhmlem  22286  evl1sca  22299  pf1ind  22320  mat1dimelbas  22436  mat1f  22447  mdetleib2  22553  mdetrsca  22568  mdetralt  22573  mdetunilem7  22583  mdetunilem9  22585  ssidcn  23220  hmphdis  23761  indishmph  23763  cmphaushmeo  23765  ordthmeolem  23766  txhmeo  23768  qtopf1  23781  ufldom  23927  symgtgp  24071  tsmsf1o  24110  iducn  24247  imasdsf1olem  24338  xpsdsval  24346  imasf1obl  24453  icchmeo  24908  iccpnfcnv  24911  xrhmeo  24913  cnheiborlem  24921  ovolctb  25457  ovoliunlem1  25469  ovoliunlem2  25470  iunmbl2  25524  dyadmbl  25567  vitalilem2  25576  vitalilem3  25577  vitalilem4  25578  vitalilem5  25579  mbfid  25602  dvid  25885  dvexp  25920  dvcnvlem  25943  dvcnv  25944  dvcnvrelem2  25985  dvcnvre  25986  efcvx  26414  reefgim  26415  efif1olem4  26509  eff1olem  26512  logrncl  26531  relogcl  26539  dvrelog  26601  relogcn  26602  logcn  26611  logf1o2  26614  dvlog  26615  dvlog2  26617  advlog  26618  advlogexp  26619  logtayl  26624  logccv  26627  dvcxp1  26704  loglesqrt  26725  asinrebnd  26865  dvatan  26899  efrlim  26933  amgmlem  26953  lgamcvg2  27018  wilthlem2  27032  wilthlem3  27033  sqff1o  27145  lgsqrlem4  27312  logdivsum  27496  log2sumbnd  27507  isismt  28602  motcl  28607  motco  28608  cnvmot  28609  motgrp  28611  motcgrg  28612  f1otrg  28939  f1otrge  28940  axlowdimlem10  29020  axcontlem5  29037  axcontlem10  29042  uspgriedgedg  29245  upgrres1  29382  umgrres1  29383  upgriseupth  30277  pliguhgr  30557  dmadjrn  31966  unopnorm  31988  unopadj  31990  unoplin  31991  counop  31992  idcnop  32052  idhmop  32053  unopbd  32086  bracnln  32180  cnvbraval  32181  leopnmid  32209  nmopleid  32210  hmopidmch  32224  hmopidmpj  32225  disjrdx  32661  fmptco1f1o  32706  isoun  32775  padct  32791  fcobij  32793  fcobijfs  32794  fcobijfs2  32795  wrdpmcl  32998  ccatws1f1o  33011  ccatws1f1olast  33012  mndlactf1o  33090  mndractf1o  33091  abliso  33096  symgfcoeu  33143  symgcom  33144  pmtrcnel  33150  pmtrcnel2  33151  pmtrcnelor  33152  wrdpmtrlast  33154  cycpmco2f1  33185  cycpmco2rn  33186  cycpmco2lem2  33188  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  cycpmconjv  33203  cycpmconjslem1  33215  cycpmconjslem2  33216  cycpmconjs  33217  islinds5  33427  ellspds  33428  1arithidomlem1  33595  1arithidomlem2  33596  1arithidom  33597  mplvrpmlem  33687  mplvrpmfgalem  33688  mplvrpmmhm  33690  mplvrpmrhm  33691  esplyfval0  33708  esplylem  33710  esplympl  33711  esplymhp  33712  esplyfv1  33713  esplyfv  33714  esplysply  33715  esplyfval3  33716  vieta  33724  tpr2rico  34056  xrge0iifmhm  34083  xrge0pluscn  34084  rrhre  34165  esumf1o  34194  volmeas  34375  eulerpartgbij  34516  eulerpartlemmf  34519  eulerpartlemgvv  34520  eulerpartlemgf  34523  eulerpartlemgs2  34524  eulerpartlemn  34525  ballotlemsima  34660  reprpmtf1o  34770  logdivsqrle  34794  hgt750lemg  34798  vonf1owev  35290  deranglem  35348  derangsn  35352  derangenlem  35353  subfacp1lem4  35365  subfacp1lem5  35366  subfacp1lem6  35367  cvmfolem  35461  cvmliftlem6  35472  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem9  37950  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  poimirlem32  37973  mblfinlem2  37979  dvasin  38025  f1ocan1fv  38047  metf1o  38076  ismtyval  38121  isismty  38122  ismtyima  38124  ismtyhmeolem  38125  ismtybndlem  38127  ismrer1  38159  reheibor  38160  grposnOLD  38203  rngoisocnv  38302  lflnegl  39522  lautset  40528  islaut  40529  lautcl  40533  lautco  40543  pautsetN  40544  ispautN  40545  ldilco  40562  ltrncoidN  40574  ltrncoval  40591  trlcoabs2N  41168  trlcoat  41169  trlcone  41174  cdlemg47a  41180  cdlemg46  41181  cdlemg47  41182  trljco  41186  tgrpgrplem  41195  tendoidcl  41215  tendo0co2  41234  tendo0pl  41237  cdlemi2  41265  cdlemk2  41278  cdlemk4  41280  cdlemk8  41284  cdlemkid2  41370  cdlemk45  41393  cdlemk53b  41402  cdlemk53  41403  cdlemk55a  41405  erng1r  41441  tendocnv  41467  dvalveclem  41471  dva0g  41473  dvhgrp  41553  dvh0g  41557  dvhopN  41562  cdlemn3  41643  cdlemn8  41650  cdlemn9  41651  dihordlem7b  41661  dihopelvalcpre  41694  dihmeetlem1N  41736  dihglblem5apreN  41737  lcfrlem13  42001  hvmapclN  42210  hvmapcl2  42212  dvrelog2  42503  dvrelog3  42504  sticksstones3  42587  sticksstones17  42602  sticksstones18  42603  sticksstones19  42604  readvrec2  42793  readvrec  42794  mapfzcons  43148  mzpresrename  43182  diophrw  43191  eldioph2  43194  diophren  43241  kelac1  43491  imasgim  43528  lnrfg  43547  nvocnvb  43849  brco2f1o  44459  brco3f1o  44460  clsneikex  44533  clsneinex  44534  clsneiel1  44535  neicvgmex  44544  neicvgel1  44546  dssmapntrcls  44555  stoweidlem27  46455  stoweidlem31  46459  stoweidlem39  46467  fourierdlem20  46555  fourierdlem50  46584  fourierdlem52  46586  fourierdlem54  46588  fourierdlem64  46598  fourierdlem76  46610  fourierdlem102  46636  fourierdlem114  46648  sge0f1o  46810  nnfoctbdjlem  46883  isomenndlem  46958  ovnsubaddlem1  46998  3f1oss1  47523  reuf1odnf  47555  reuf1od  47556  f1oresf1o2  47739  fundcmpsurbijinjpreimafv  47867  fundcmpsurinjimaid  47871  grimfn  48355  isgrim  48358  grimuhgr  48363  grimco  48365  uhgrimedgi  48366  isuspgrim0lem  48369  isuspgrim0  48370  isuspgrim  48372  upgrimwlklem4  48376  gricushgr  48393  isubgrgrim  48405  uhgrimisgrgriclem  48406  uhgrimisgrgric  48407  clnbgrgrim  48410  grimedg  48411  grtriclwlk3  48421  isubgr3stgrlem3  48444  isubgr3stgrlem4  48445  isubgr3stgrlem6  48447  isubgr3stgrlem7  48448  isubgr3stgrlem8  48449  isubgr3stgrlem9  48450  grlimfn  48455  isgrlim  48458  uspgrlimlem1  48464  uspgrlimlem2  48465  uspgrlimlem3  48466  uspgrlimlem4  48467  grlimprclnbgredg  48473  grlimgredgex  48476  grlimgrtrilem2  48478  grlictr  48491  clnbgr3stgrgrlim  48495  clnbgr3stgrgrlic  48496  1hegrlfgr  48608  funcringcsetcALTV2lem8  48773  funcringcsetclem8ALTV  48796  itcovalendof  49145  uptrlem1  49685  uptr2  49696  swapf2f1oaALT  49753  swapfcoa  49756  swapffunc  49757  fucoppc  49885  thincciso  49928  thinccisod  49929  lmdran  50146  cmdlan  50147  amgmwlem  50277