Theorem fveq1 6877

Description: Equality theorem for function value. (Contributed by NM, 29-Dec-1996.)

Assertion

Ref	Expression
fveq1	⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Proof of Theorem fveq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq 5105	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6517	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6541	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6541	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2820	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5103  ℩cio 6487  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541

This theorem is used by:  fveq1i  6879  fveq1d  6880  iffv  6895  fvmptd3f  7002  fvmptdv2  7005  eqfnun  7029  fsnex  7284  f1prex  7285  isoeq1  7318  oveq  7419  elovmpt3imp  7671  ofrfvalg  7686  offval  7687  offval3  7979  bropopvvv  8087  bropfvvvvlem  8088  poseq  8156  soseq  8157  frrlem1  8285  frrlem13  8297  smoeq  8339  tfrlem12  8378  tz7.44-2  8396  tz7.44-3  8397  rdgeq1  8400  fsetfocdm  8862  fsetprcnex  8863  mapsncnv  8900  elixp2  8908  resixpfo  8943  elixpsn  8944  mapsnend  9043  enfixsn  9084  mapxpen  9141  ac6sfi  9254  ordtypelem7  9496  wemaplem1  9518  ixpiunwdom  9562  oemapval  9662  cantnf  9672  wemapwe  9676  cnfcom3clem  9684  ssttrcl  9694  ttrcltr  9695  ttrclss  9699  ttrclselem2  9705  updjud  9939  infxpenc2lem2  10023  fseqenlem1  10027  dfac8clem  10035  ac5num  10039  acni  10048  acni2  10049  acnlem  10051  dfac4  10125  dfac5lem5  10130  dfac2a  10132  dfac9  10139  dfacacn  10144  dfac12lem1  10146  dfac12r  10149  cofsmo  10271  cfsmolem  10272  cfsmo  10273  cfcoflem  10274  coftr  10275  alephsing  10278  isfin3ds  10331  fin23lem17  10340  fin23lem32  10346  fin23lem39  10352  isf33lem  10368  isf34lem6  10382  axcc2lem  10438  axcc3  10440  axdc2lem  10450  axdc3lem2  10453  axdc3lem3  10454  axdc3  10456  axdc4lem  10457  axcclem  10459  ac6num  10481  axdclem2  10522  konigthlem  10577  inar1  10784  1fv  13702  axdc4uzlem  14047  seqeq3  14070  seqof  14123  ccatfval  14638  wrdl1s1  14682  ccat1st1st  14696  cshf1  14881  cshweqrep  14892  wrdlen2i  15013  wwlktovf  15029  wwlktovf1  15030  wwlktovfo  15031  wrd2f1tovbij  15033  rtrclreclem1  15130  dfrtrclrec2  15131  rtrclreclem2  15132  rtrclreclem4  15134  dfrtrcl2  15135  clim  15581  rlim  15582  ello1  15602  elo1  15613  summo  15803  fsum  15806  prodmo  16023  fprod  16028  bpolylem  16134  bpolyval  16135  vdwlem6  17078  vdwlem8  17080  ramcl  17121  strfvnd  17277  prdsplusgval  17558  prdsmulrval  17560  prdsleval  17562  prdsdsval  17563  prdsvscaval  17564  xpsff1o  17653  isacs2  17741  isnat  18039  yonedalem3b  18367  yonedainv  18369  ischn  18695  chnind  18709  chnub  18710  ismgmhm  18798  ismhm  18893  prdspjmhm  18938  isgrpinv  19117  pwsmulg  19242  isghm  19343  cayleylem2  19540  symgfix2  19543  gsmsymgrfix  19555  gsmsymgreq  19559  symgfixelq  19560  pmtr3ncomlem2  19601  pmtrdifel  19607  pmtrdifwrdel  19612  pmtrdifwrdel2  19613  psgnunilem2  19622  psgnunilem3  19623  efgsdm  19857  efgredlemd  19871  efgredlem  19874  efgred  19875  efgrelexlema  19876  efgrelexlemb  19877  prdsgsum  20108  pwspjmhmmgpd  20468  pwsexpg  20469  pwsgprod  20470  isrnghm  20582  isrhm0  20617  isabv  20977  islmhm  21211  frgpcyg  21786  psgndiflemB  21813  psgndiflemA  21814  dsmmelbas  21952  frlmipval  21992  frlmphl  21994  uvcf1  22005  islindf  22025  islindf4  22051  psrmulfval  22158  evlslem2  22295  evlslem3  22296  evlslem1  22298  mpfrcl  22301  evlsvval  22306  evlsvvval  22309  selvval  22336  mplmapghm  22338  evlsvarval  22343  selvvvval  22358  psdval  22387  psdcoef  22388  psdadd  22391  psdmul  22394  psdmvr  22397  coe1fval  22430  coe1mul2lem2  22494  coe1tm  22499  madetsumid  22683  mvmulval  22765  marepvval0  22788  mulmarep1gsum2  22796  mdetleib2  22810  m1detdiag  22819  mdetralt  22830  mdetunilem7  22840  mdetunilem9  22842  m2detleiblem3  22851  m2detleiblem4  22852  m2detleib  22853  symgmatr01lem  22875  gsummatr01lem1  22877  gsummatr01lem4  22880  gsummatr01  22881  smadiadetlem3  22890  matunitlindflem2  22902  pmatcoe1fsupp  22926  pmatcollpw3lem  23008  pmatcollpw3fi1lem2  23012  iscnp  23462  1stcfb  23670  ptpjpre1  23797  elpt  23798  elptr  23799  ptpjopn  23838  dfac14  23844  upxp  23849  pthaus  23864  ptrescn  23865  xkoptsub  23880  cnmptkp  23906  xkofvcn  23910  cnmptk1p  23911  cnmptk2  23912  ptunhmeo  24034  ptcmplem3  24280  ptcmplem4  24281  symgtgp  24332  prdstmdd  24350  isucn  24503  imasdsf1olem  24599  prdsxmslem2  24755  tngngp3  24882  nmoval  24941  elcncf  25117  ishtpy  25200  pcoval  25239  om1elbas  25260  elpi1i  25274  iscau  25504  rrxds  25621  rrxdsfival  25641  ehl1eudisval  25649  ehl2eudisval  25651  mbfi1fseqlem6  25948  mbfi1flimlem  25950  isibl  25993  deg1ldg  26317  deg1leb  26320  elply2  26421  elplyr  26426  ne0p  26432  coeeu  26451  coelem  26452  coeeq  26453  coeidlem  26463  elqaalem3  26553  preimaaa  26555  qaa  26556  iaaOLD  26561  aareccl  26562  aannenlem2  26565  aaliou2  26576  dchrptlem2  27501  dchrpt  27503  dchrsum2  27504  sumdchr2  27506  dchrvmaeq0  27740  rpvmasum2  27748  dchrisum0re  27749  ostth  27875  ltsval  27883  nolesgn2o  27907  nogesgn1o  27909  noresle  27933  nosupprefixmo  27936  noinfprefixmo  27937  nosupcbv  27938  nosupfv  27942  noinfcbv  27953  noinffv  27957  iscgrg  28854  isismt  28876  israg  29051  elcgrabasi  29254  elcgrabasrd  29255  cgrabasimass  29257  iseqlg  29291  brbtwn  29356  brbtwn2  29362  colinearalg  29367  axsegconlem1  29374  axsegcon  29384  ax5seglem5  29390  axpasch  29398  axlowdim  29418  axeuclidlem  29419  axcontlem1  29421  axcontlem2  29422  axcontlem5  29425  vtxdgfval  29927  1egrvtxdg1  29969  isewlk  30062  iswlk  30070  uspgr2wlkeq2  30106  iswlkon  30115  isclwlk  30239  iscrct  30256  iscycl  30257  iswwlks  30304  wwlknon  30325  wlkiswwlks2  30343  wwlksnredwwlkn0  30364  wlksnwwlknvbij  30376  wwlksnextproplem3  30379  wwlksnextprop  30380  umgr2wlk  30417  midwwlks2s3  30420  elwwlks2  30437  elwspths2spth  30438  rusgrnumwwlkslem  30440  rusgrnumwwlkb0  30442  rusgrnumwwlks  30445  isclwwlk  30454  clwlkclwwlklem1  30469  clwwlkn1loopb  30513  clwwlkel  30516  clwwlkf  30517  clwwlkf1  30519  isclwwlknon  30561  clwwlknon1  30567  s2elclwwlknon2  30574  clwwlkvbij  30583  loop1cycl  30623  uhgr3cyclex  30662  fusgreg2wsplem  30813  fusgr2wsp2nb  30814  fusgreghash2wsp  30818  2clwwlkel  30829  extwwlkfabel  30833  numclwwlk1lem2fv  30836  numclwwlk1lem2  30840  clwwlknonclwlknonf1o  30842  dlwwlknondlwlknonf1o  30845  numclwwlk2lem1  30856  numclwlk2lem2f  30857  numclwlk2lem2f1o  30859  ex-fv  30923  isnvlem  31091  islno  31234  nmooval  31244  nmblolbi  31281  isphg  31298  ajmoi  31339  ajval  31342  ubthlem3  31353  htthlem  31398  hcau  31665  hlimi  31669  hosmval  32216  hommval  32217  hodmval  32218  hfsmval  32219  hfmmval  32220  adjmo  32313  nmopval  32337  elcnop  32338  ellnop  32339  elunop  32353  elhmop  32354  nmfnval  32357  elcnfn  32363  ellnfn  32364  adjeu  32370  adjval  32371  eigvecval  32377  eigvalfval  32378  adj1  32414  adjeq  32416  hmopadj2  32422  lnopeq0i  32488  lnopeq  32490  elunop2  32494  lnophm  32500  hmopco  32504  nmbdoplb  32506  nmcoplb  32511  lnopcon  32516  lnfn0  32528  lnfnmul  32529  nmbdfnlb  32531  nmcfnlb  32535  lnfncon  32537  riesz4  32545  riesz1  32546  cnlnadjlem9  32556  cnlnadjeu  32559  cnlnssadj  32561  nmopcoi  32576  bra11  32589  cnvbraval  32591  pjss2coi  32645  pjssdif2i  32655  pjssdif1i  32656  pjclem4  32680  pj3si  32688  pj3cor1i  32690  isst  32694  ishst  32695  stri  32738  hstri  32746  aciunf1lem  33135  ismnt  33423  mgcval  33427  fzo0pmtrlast  33532  elrgspnlem1  33682  elrgspnlem2  33683  elrgspnlem3  33684  elrgspnlem4  33685  elrgspn  33686  elrgspnsubrunlem1  33687  linds2eq  33814  elrspunidl  33856  elrspunsn  33857  dfufd2lem  33959  psrnzr  34022  0mplrim  34024  0mplric  34025  selvply1rhmlema  34028  selvply1rhmlemb  34029  selvply1rhmlem1  34030  selvply1rhmlem3  34032  selvply1rhmlem5  34034  selvply1rhm  34035  mplidom  34038  extvfv  34043  extvfvv  34044  extvfvcl  34046  evlvarval  34051  evlextv  34052  mplvrpmga  34055  splysubrg  34070  issply  34071  vietalem  34089  vieta  34090  lbsdiflsp0  34136  fedgmullem1  34139  fedgmullem2  34140  fedgmul  34141  fldextrspunlsplem  34183  fldextrspunlsp  34184  fldext2chn  34238  constrextdg2lem  34258  constrextdg2  34259  lmatval  34323  mdetpmtr1  34333  zarcmplem  34391  ismeas  34710  isrnmeas  34711  cntnevol  34739  carsgval  34814  sitgval  34843  eulerpartleme  34874  eulerpartlemd  34877  eulerpartlemr  34885  eulerpartlemgvv  34887  eulerpart  34893  cndprobval  34944  signstfvneq0  35080  reprsum  35121  reprsuc  35123  reprpmtf1o  35134  reprdifc  35135  breprexp  35141  vtsval  35145  hgt750lemb  35164  hgt750lema  35165  hgt750leme  35166  bnj66  35369  bnj106  35377  bnj125  35381  bnj154  35387  bnj155  35388  bnj526  35397  bnj540  35401  bnj609  35426  bnj611  35427  bnj893  35437  bnj1000  35450  bnj1014  35470  bnj1015  35471  bnj1234  35522  bnj1463  35564  fineqvnttrclse  35650  gblacfnacd  35699  derangenlem  35750  subfacp1lem3  35761  subfacp1lem5  35763  subfacp1lem6  35764  subfacp1  35765  sconnpht  35808  cnpconn  35809  txpconn  35811  ptpconn  35812  indispconn  35813  connpconn  35814  cvxpconn  35821  cvmliftmo  35863  cvmliftlem14  35876  cvmliftlem15  35877  cvmliftiota  35880  cvmlift2  35895  cvmliftphtlem  35896  cvmlift3lem2  35899  cvmlift3lem6  35903  cvmlift3lem7  35904  cvmlift3lem9  35906  cvmlift3  35907  satfv1lem  35941  satfv1  35942  sategoelfvb  35998  mrsubff1  36093  mrsub0  36095  mrsubccat  36097  mrsubcn  36098  elmsubrn  36107  msubrn  36108  msubco  36110  msubvrs  36139  mclsax  36148  shftvalg  36311  fwddifval  36742  fwddifnval  36743  bj-evalval  37825  unceq  38355  poimirlem17  38386  poimirlem20  38389  poimirlem22  38391  poimirlem23  38392  poimirlem27  38396  poimirlem28  38397  poimirlem30  38399  poimirlem31  38400  poimirlem32  38401  poimir  38402  broucube  38403  voliunnfl  38413  volsupnfl  38414  itg2addnclem  38420  itg2addnclem3  38422  itg2addnc  38423  ftc1anclem2  38443  ftc1anclem5  38446  upixp  38479  fdc  38495  isismty  38551  rrnmval  38578  elghomlem2OLD  38636  isrngohom  38715  islfl  39933  isopos  40053  islaut  40956  ispautN  40972  isldil  40983  isltrn  40992  ltrnid  41008  ltrneq2  41021  isdilN  41027  istrnN  41030  trlval  41035  ltrneq3  41081  cdleme50ex  41432  cdleme  41433  cdlemg1a  41443  ltrniotaval  41454  ltrniotavalbN  41457  cdlemeiota  41458  cdlemg2jlemOLDN  41466  cdlemg2fvlem  41467  cdlemg2klem  41468  istendo  41633  tendoplcbv  41648  tendopl  41649  tendoicbv  41666  tendoi  41667  tendoid0  41698  tendo1ne0  41701  cdlemksv2  41720  cdlemkuv2  41740  cdlemk33N  41782  cdlemk34  41783  cdlemk36  41786  cdlemk19u  41843  cdlemk  41847  tendoex  41848  dvavsca  41890  dvhvscacbv  41971  dvhvscaval  41972  dicopelval  42050  dicelval1sta  42060  diclspsn  42067  dihmeetlem13N  42192  dih1dimatlem0  42201  dih1dimatlem  42202  dihpN  42209  islpolN  42356  hdmap1fval  42669  hdmapfval  42700  sticksstones1  43012  sticksstones2  43013  sticksstones3  43014  sticksstones8  43019  sticksstones10  43021  sticksstones11  43022  sticksstones12a  43023  sticksstones12  43024  sticksstones15  43027  frlmsnic  43422  uvcn0  43424  evlsbagval  43432  evlselv  43435  fsuppssindlem2  43438  fsuppssind  43439  prjspnfv01  43470  prjspner01  43471  prjspner1  43472  sn-isghm  43519  ismrc  43546  mzpclval  43570  mzpsubst  43593  mzprename  43594  mzpcompact2lem  43596  eldioph  43603  eldioph2  43607  eldioph2b  43608  eldioph3  43611  rexrabdioph  43635  2rexfrabdioph  43637  3rexfrabdioph  43638  4rexfrabdioph  43639  6rexfrabdioph  43640  7rexfrabdioph  43641  eldioph4i  43653  rabren3dioph  43656  mzpcong  43813  jm2.27dlem1  43850  wepwsolem  43883  aomclem6  43900  aomclem8  43902  dfac11  43903  dgraalem  43986  dgraaub  43989  dgraa0p  43990  mpaaeu  43991  mpaalem  43993  aaitgo  44003  rngunsnply  44010  cantnfresb  44165  tfsconcatun  44178  nvocnvb  44262  eliunov2  44519  rfovcnvfvd  44847  fsovfvd  44850  fsovcnvlem  44853  dssmapfv2d  44858  dssmapnvod  44860  clsk1independent  44886  ntrclskb  44909  ntrclsk13  44911  gneispace2  44972  mnringmulrvald  45065  dvconstbi  45158  addrval  45288  subrval  45289  mulvval  45290  relpeq1  45767  fnchoice  45863  refsum2cnlem1  45871  choicefi  46031  axccdom  46052  fmulcl  46411  fmuldfeqlem1  46412  mccllem  46427  mccl  46428  climf  46452  climf2  46494  dvnprodlem1  46774  dvnprodlem3  46776  dvnprod  46777  stoweidlem2  46830  stoweidlem6  46834  stoweidlem8  46836  stoweidlem9  46837  stoweidlem15  46843  stoweidlem16  46844  stoweidlem17  46845  stoweidlem18  46846  stoweidlem21  46849  stoweidlem27  46855  stoweidlem31  46859  stoweidlem36  46864  stoweidlem37  46865  stoweidlem41  46869  stoweidlem43  46871  stoweidlem44  46872  stoweidlem45  46873  stoweidlem46  46874  stoweidlem48  46876  stoweidlem51  46879  stoweidlem55  46883  stoweidlem59  46887  stoweidlem60  46888  stoweidlem62  46890  fourierdlem2  46937  fourierdlem3  46938  elaa2lem  47061  etransclem11  47073  etransclem24  47086  etransclem26  47088  etransclem28  47090  etransclem35  47097  rrndistlt  47118  ioorrnopn  47133  subsaliuncllem  47185  sge0val  47194  ismea  47279  caragenval  47321  isome  47322  isomenndlem  47358  hoicvrrex  47384  ovnlecvr  47386  ovncvrrp  47392  ovn0lem  47393  ovnsubaddlem1  47398  ovnsubadd  47400  hsphoif  47404  hoidmvval  47405  hsphoival  47407  hoidmvlelem3  47425  hoidmvlelem5  47427  hoidmvle  47428  ovnhoilem1  47429  ovnhoi  47431  ovnlecvr2  47438  ovncvr2  47439  hoidifhspval2  47443  hoiqssbllem2  47451  hspmbllem2  47455  hspmbllem3  47456  hspmbl  47457  ovnovollem1  47484  smfmullem2  47620  smfmul  47623  smfpimcclem  47635  chnerlem1  47710  sqrtnnaa  47731  sqrtnzqaa  47732  sinnpoly  47759  cfsetsnfsetfv  47945  cfsetsnfsetfo  47948  iccpart  48316  iccpartiun  48334  icceuelpart  48336  nnsum3primes4  48704  nnsum3primesgbe  48708  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  bgoldbtbnd  48725  isisubgr  48778  isgrim  48798  grimidvtxedg  48801  grimcnv  48804  grimco  48805  isuspgrim0  48810  gricushgr  48833  ushggricedg  48843  uhgrimisgrgric  48847  isgrtri  48859  isubgr3stgrlem3  48884  isubgr3stgr  48891  isgrlim  48898  uspgrlim  48908  grlicref  48928  grlicsym  48929  grlictr  48931  grlimedgnedg  49047  isupwlk  49052  lincval  49339  lincdifsn  49354  linindslinci  49378  lindslinindsimp1  49387  linds0  49395  el0ldep  49396  lindsrng01  49398  snlindsntorlem  49400  ldepspr  49403  islindeps2  49413  zlmodzxzldep  49434  bigoval  49479  elbigo  49481  0aryfvalelfv  49565  1arympt1fv  49569  1arymaptfv  49570  1arymaptfo  49573  2arymptfv  49580  2arymaptfv  49581  2arymaptfo  49584  prelrrx2b  49644  rrx2plord  49650  rrx2vlinest  49671  rrx2linesl  49673  elrrx2linest2  49675  line2ylem  49681  line2xlem  49683  itsclc0  49701  itsclc0b  49702  itscnhlinecirc02p  49715  elfvne0  49777  iinfprg  49985  thincciso  50379  thinccisod  50380  setrecseq  50611  aacllem  50772  crosspval  50787  crosspdot0lem  50796  veronesevald  50804