Theorem fveq1 6882

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 6521	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6545	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6545	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2821	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545

This theorem is used by:  fveq1i  6884  fveq1d  6885  iffv  6900  fvmptd3f  7007  fvmptdv2  7010  eqfnun  7034  fsnex  7289  f1prex  7290  isoeq1  7323  oveq  7424  elovmpt3imp  7676  ofrfvalg  7699  offval  7700  offval3  7992  bropopvvv  8099  bropfvvvvlem  8100  poseq  8168  soseq  8169  frrlem1  8297  frrlem13  8309  smoeq  8351  tfrlem12  8390  tz7.44-2  8408  tz7.44-3  8409  rdgeq1  8412  fsetfocdm  8876  fsetprcnex  8877  mapsncnv  8914  elixp2  8922  resixpfo  8957  elixpsn  8958  mapsnend  9057  enfixsn  9098  mapxpen  9155  ac6sfi  9268  ordtypelem7  9511  wemaplem1  9533  ixpiunwdom  9577  oemapval  9677  cantnf  9687  wemapwe  9691  cnfcom3clem  9699  ssttrcl  9709  ttrcltr  9710  ttrclss  9714  ttrclselem2  9720  updjud  10008  infxpenc2lem2  10092  fseqenlem1  10096  dfac8clem  10104  ac5num  10108  acni  10117  acni2  10118  acnlem  10120  dfac4  10194  dfac5lem5  10199  dfac2a  10201  dfac9  10208  dfacacn  10213  dfac12lem1  10215  dfac12r  10218  cofsmo  10340  cfsmolem  10341  cfsmo  10342  cfcoflem  10343  coftr  10344  alephsing  10347  isfin3ds  10400  fin23lem17  10409  fin23lem32  10415  fin23lem39  10421  isf33lem  10437  isf34lem6  10451  axcc2lem  10507  axcc3  10509  axdc2lem  10519  axdc3lem2  10522  axdc3lem3  10523  axdc3  10525  axdc4lem  10526  axcclem  10528  ac6num  10550  axdclem2  10591  konigthlem  10646  inar1  10853  1fv  13774  axdc4uzlem  14119  seqeq3  14142  seqof  14195  ccatfval  14711  wrdl1s1  14755  ccat1st1st  14769  cshf1  14954  cshweqrep  14965  wrdlen2i  15086  wwlktovf  15102  wwlktovf1  15103  wwlktovfo  15104  wrd2f1tovbij  15106  rtrclreclem1  15203  dfrtrclrec2  15204  rtrclreclem2  15205  rtrclreclem4  15207  dfrtrcl2  15208  clim  15654  rlim  15655  ello1  15675  elo1  15686  summo  15876  fsum  15879  prodmo  16096  fprod  16101  bpolylem  16207  bpolyval  16208  vdwlem6  17157  vdwlem8  17159  ramcl  17200  strfvnd  17356  prdsplusgval  17637  prdsmulrval  17639  prdsleval  17641  prdsdsval  17642  prdsvscaval  17643  xpsff1o  17732  isacs2  17820  isnat  18118  yonedalem3b  18446  yonedainv  18448  ischn  18774  chnind  18788  chnub  18789  ismgmhm  18878  ismhm  18973  prdspjmhm  19018  isgrpinv  19197  pwsmulg  19322  isghm  19423  cayleylem2  19620  symgfix2  19623  gsmsymgrfix  19635  gsmsymgreq  19639  symgfixelq  19640  pmtr3ncomlem2  19681  pmtrdifel  19687  pmtrdifwrdel  19692  pmtrdifwrdel2  19693  psgnunilem2  19702  psgnunilem3  19703  efgsdm  19937  efgredlemd  19951  efgredlem  19954  efgred  19955  efgrelexlema  19956  efgrelexlemb  19957  prdsgsum  20188  pwspjmhmmgpd  20550  pwsexpg  20551  pwsgprod  20552  isrnghm  20664  isrhm0  20699  isabv  21061  islmhm  21295  frgpcyg  21872  psgndiflemB  21899  psgndiflemA  21900  dsmmelbas  22038  frlmipval  22078  frlmphl  22080  uvcf1  22091  islindf  22111  islindf4  22137  psrmulfval  22244  evlslem2  22381  evlslem3  22382  evlslem1  22384  mpfrcl  22387  evlsvval  22392  evlsvvval  22395  selvval  22422  mplmapghm  22424  evlsvarval  22429  selvvvval  22444  psdval  22473  psdcoef  22474  psdadd  22477  psdmul  22480  psdmvr  22483  coe1fval  22516  coe1mul2lem2  22580  coe1tm  22585  madetsumid  22769  mvmulval  22851  marepvval0  22874  mulmarep1gsum2  22882  mdetleib2  22896  m1detdiag  22905  mdetralt  22916  mdetunilem7  22926  mdetunilem9  22928  m2detleiblem3  22937  m2detleiblem4  22938  m2detleib  22939  symgmatr01lem  22961  gsummatr01lem1  22963  gsummatr01lem4  22966  gsummatr01  22967  smadiadetlem3  22976  matunitlindflem2  22988  pmatcoe1fsupp  23012  pmatcollpw3lem  23094  pmatcollpw3fi1lem2  23098  iscnp  23548  1stcfb  23756  ptpjpre1  23883  elpt  23884  elptr  23885  ptpjopn  23924  dfac14  23930  upxp  23935  pthaus  23950  ptrescn  23951  xkoptsub  23966  cnmptkp  23992  xkofvcn  23996  cnmptk1p  23997  cnmptk2  23998  ptunhmeo  24120  ptcmplem3  24366  ptcmplem4  24367  symgtgp  24418  prdstmdd  24436  isucn  24589  imasdsf1olem  24685  prdsxmslem2  24841  tngngp3  24968  nmoval  25027  elcncf  25203  ishtpy  25286  pcoval  25325  om1elbas  25346  elpi1i  25360  iscau  25590  rrxds  25707  rrxdsfival  25727  ehl1eudisval  25735  ehl2eudisval  25737  mbfi1fseqlem6  26034  mbfi1flimlem  26036  isibl  26079  deg1ldg  26403  deg1leb  26406  elply2  26507  elplyr  26512  ne0p  26518  coeeu  26537  coelem  26538  coeeq  26539  coeidlem  26549  elqaalem3  26637  preimaaa  26639  qaa  26640  iaaOLD  26645  aareccl  26646  aannenlem2  26649  aaliou2  26660  dchrptlem2  27585  dchrpt  27587  dchrsum2  27588  sumdchr2  27590  dchrvmaeq0  27824  rpvmasum2  27832  dchrisum0re  27833  ostth  27959  ltsval  27997  nolesgn2o  28021  nogesgn1o  28023  noresle  28047  nosupprefixmo  28050  noinfprefixmo  28051  nosupcbv  28052  nosupfv  28056  noinfcbv  28067  noinffv  28071  iscgrg  28968  isismt  28990  israg  29165  elcgrabasi  29368  elcgrabasrd  29369  cgrabasimass  29371  iseqlg  29405  brbtwn  29470  brbtwn2  29476  colinearalg  29481  axsegconlem1  29488  axsegcon  29498  ax5seglem5  29504  axpasch  29512  axlowdim  29532  axeuclidlem  29533  axcontlem1  29535  axcontlem2  29536  axcontlem5  29539  vtxdgfval  30041  1egrvtxdg1  30083  isewlk  30176  iswlk  30184  uspgr2wlkeq2  30220  iswlkon  30229  isclwlk  30353  iscrct  30370  iscycl  30371  iswwlks  30418  wwlknon  30439  wlkiswwlks2  30457  wwlksnredwwlkn0  30478  wlksnwwlknvbij  30490  wwlksnextproplem3  30493  wwlksnextprop  30494  umgr2wlk  30531  midwwlks2s3  30534  elwwlks2  30551  elwspths2spth  30552  rusgrnumwwlkslem  30554  rusgrnumwwlkb0  30556  rusgrnumwwlks  30559  isclwwlk  30568  clwlkclwwlklem1  30583  clwwlkn1loopb  30627  clwwlkel  30630  clwwlkf  30631  clwwlkf1  30633  isclwwlknon  30675  clwwlknon1  30681  s2elclwwlknon2  30688  clwwlkvbij  30697  loop1cycl  30737  uhgr3cyclex  30776  fusgreg2wsplem  30927  fusgr2wsp2nb  30928  fusgreghash2wsp  30932  2clwwlkel  30943  extwwlkfabel  30947  numclwwlk1lem2fv  30950  numclwwlk1lem2  30954  clwwlknonclwlknonf1o  30956  dlwwlknondlwlknonf1o  30959  numclwwlk2lem1  30970  numclwlk2lem2f  30971  numclwlk2lem2f1o  30973  ex-fv  31037  isnvlem  31205  islno  31348  nmooval  31358  nmblolbi  31395  isphg  31412  ajmoi  31453  ajval  31456  ubthlem3  31467  htthlem  31512  hcau  31779  hlimi  31783  hosmval  32330  hommval  32331  hodmval  32332  hfsmval  32333  hfmmval  32334  adjmo  32427  nmopval  32451  elcnop  32452  ellnop  32453  elunop  32467  elhmop  32468  nmfnval  32471  elcnfn  32477  ellnfn  32478  adjeu  32484  adjval  32485  eigvecval  32491  eigvalfval  32492  adj1  32528  adjeq  32530  hmopadj2  32536  lnopeq0i  32602  lnopeq  32604  elunop2  32608  lnophm  32614  hmopco  32618  nmbdoplb  32620  nmcoplb  32625  lnopcon  32630  lnfn0  32642  lnfnmul  32643  nmbdfnlb  32645  nmcfnlb  32649  lnfncon  32651  riesz4  32659  riesz1  32660  cnlnadjlem9  32670  cnlnadjeu  32673  cnlnssadj  32675  nmopcoi  32690  bra11  32703  cnvbraval  32705  pjss2coi  32759  pjssdif2i  32769  pjssdif1i  32770  pjclem4  32794  pj3si  32802  pj3cor1i  32804  isst  32808  ishst  32809  stri  32852  hstri  32860  aciunf1lem  33249  ismnt  33537  mgcval  33541  fzo0pmtrlast  33646  elrgspnlem1  33796  elrgspnlem2  33797  elrgspnlem3  33798  elrgspnlem4  33799  elrgspn  33800  elrgspnsubrunlem1  33801  linds2eq  33929  elrspunidl  33971  elrspunsn  33972  dfufd2lem  34074  psrnzr  34137  0mplrim  34139  0mplric  34140  selvply1rhmlema  34143  selvply1rhmlemb  34144  selvply1rhmlem1  34145  selvply1rhmlem3  34147  selvply1rhmlem5  34149  selvply1rhm  34150  mplidom  34153  extvfv  34158  extvfvv  34159  extvfvcl  34161  evlvarval  34166  evlextv  34167  mplvrpmga  34170  splysubrg  34185  issply  34186  vietalem  34204  vieta  34205  lbsdiflsp0  34251  fedgmullem1  34254  fedgmullem2  34255  fedgmul  34256  fldextrspunlsplem  34298  fldextrspunlsp  34299  fldext2chn  34353  constrextdg2lem  34373  constrextdg2  34374  lmatval  34438  mdetpmtr1  34448  zarcmplem  34506  ismeas  34825  isrnmeas  34826  cntnevol  34854  carsgval  34928  sitgval  34957  eulerpartleme  34988  eulerpartlemd  34991  eulerpartlemr  34999  eulerpartlemgvv  35001  eulerpart  35007  cndprobval  35058  signstfvneq0  35194  reprsum  35235  reprsuc  35237  reprpmtf1o  35248  reprdifc  35249  breprexp  35255  vtsval  35259  hgt750lemb  35278  hgt750lema  35279  hgt750leme  35280  bnj66  35483  bnj106  35491  bnj125  35495  bnj154  35501  bnj155  35502  bnj526  35511  bnj540  35515  bnj609  35540  bnj611  35541  bnj893  35551  bnj1000  35564  bnj1014  35584  bnj1015  35585  bnj1234  35636  bnj1463  35678  fineqvnttrclse  35775  gblacfnacd  35864  derangenlem  35915  subfacp1lem3  35926  subfacp1lem5  35928  subfacp1lem6  35929  subfacp1  35930  sconnpht  35973  cnpconn  35974  txpconn  35976  ptpconn  35977  indispconn  35978  connpconn  35979  cvxpconn  35986  cvmliftmo  36028  cvmliftlem14  36041  cvmliftlem15  36042  cvmliftiota  36045  cvmlift2  36060  cvmliftphtlem  36061  cvmlift3lem2  36064  cvmlift3lem6  36068  cvmlift3lem7  36069  cvmlift3lem9  36071  cvmlift3  36072  satfv1lem  36106  satfv1  36107  sategoelfvb  36163  mrsubff1  36258  mrsub0  36260  mrsubccat  36262  mrsubcn  36263  elmsubrn  36272  msubrn  36273  msubco  36275  msubvrs  36304  mclsax  36313  shftvalg  36476  fwddifval  36907  fwddifnval  36908  bj-evalval  37976  unceq  38504  poimirlem17  38535  poimirlem20  38538  poimirlem22  38540  poimirlem23  38541  poimirlem27  38545  poimirlem28  38546  poimirlem30  38548  poimirlem31  38549  poimirlem32  38550  poimir  38551  broucube  38552  voliunnfl  38562  volsupnfl  38563  itg2addnclem  38569  itg2addnclem3  38571  itg2addnc  38572  ftc1anclem2  38592  ftc1anclem5  38595  upixp  38643  fdc  38659  isismty  38715  rrnmval  38742  elghomlem2OLD  38800  isrngohom  38879  islfl  40097  isopos  40217  islaut  41120  ispautN  41136  isldil  41147  isltrn  41156  ltrnid  41172  ltrneq2  41185  isdilN  41191  istrnN  41194  trlval  41199  ltrneq3  41245  cdleme50ex  41596  cdleme  41597  cdlemg1a  41607  ltrniotaval  41618  ltrniotavalbN  41621  cdlemeiota  41622  cdlemg2jlemOLDN  41630  cdlemg2fvlem  41631  cdlemg2klem  41632  istendo  41797  tendoplcbv  41812  tendopl  41813  tendoicbv  41830  tendoi  41831  tendoid0  41862  tendo1ne0  41865  cdlemksv2  41884  cdlemkuv2  41904  cdlemk33N  41946  cdlemk34  41947  cdlemk36  41950  cdlemk19u  42007  cdlemk  42011  tendoex  42012  dvavsca  42054  dvhvscacbv  42135  dvhvscaval  42136  dicopelval  42214  dicelval1sta  42224  diclspsn  42231  dihmeetlem13N  42356  dih1dimatlem0  42365  dih1dimatlem  42366  dihpN  42373  islpolN  42520  hdmap1fval  42833  hdmapfval  42864  sticksstones1  43176  sticksstones2  43177  sticksstones3  43178  sticksstones8  43183  sticksstones10  43185  sticksstones11  43186  sticksstones12a  43187  sticksstones12  43188  sticksstones15  43191  frlmsnic  43584  uvcn0  43586  evlsbagval  43594  evlselv  43597  fsuppssindlem2  43600  fsuppssind  43601  frlmnzcoordval  43633  sn-isghm  43664  ismrc  43691  mzpclval  43715  mzpsubst  43738  mzprename  43739  mzpcompact2lem  43741  eldioph  43748  eldioph2  43752  eldioph2b  43753  eldioph3  43756  rexrabdioph  43780  2rexfrabdioph  43782  3rexfrabdioph  43783  4rexfrabdioph  43784  6rexfrabdioph  43785  7rexfrabdioph  43786  eldioph4i  43798  rabren3dioph  43801  mzpcong  43958  jm2.27dlem1  43995  wepwsolem  44028  aomclem6  44045  aomclem8  44047  dfac11  44048  dgraalem  44131  dgraaub  44134  dgraa0p  44135  mpaaeu  44136  mpaalem  44138  aaitgo  44148  rngunsnply  44155  cantnfresb  44310  tfsconcatun  44323  nvocnvb  44407  eliunov2  44664  rfovcnvfvd  44992  fsovfvd  44995  fsovcnvlem  44998  dssmapfv2d  45003  dssmapnvod  45005  clsk1independent  45031  ntrclskb  45054  ntrclsk13  45056  gneispace2  45117  mnringmulrvald  45210  dvconstbi  45303  addrval  45433  subrval  45434  mulvval  45435  relpeq1  45912  fnchoice  46015  refsum2cnlem1  46023  choicefi  46183  axccdom  46204  fmulcl  46562  fmuldfeqlem1  46563  mccllem  46578  mccl  46579  climf  46603  climf2  46645  dvnprodlem1  46925  dvnprodlem3  46927  dvnprod  46928  stoweidlem2  46981  stoweidlem6  46985  stoweidlem8  46987  stoweidlem9  46988  stoweidlem15  46994  stoweidlem16  46995  stoweidlem17  46996  stoweidlem18  46997  stoweidlem21  47000  stoweidlem27  47006  stoweidlem31  47010  stoweidlem36  47015  stoweidlem37  47016  stoweidlem41  47020  stoweidlem43  47022  stoweidlem44  47023  stoweidlem45  47024  stoweidlem46  47025  stoweidlem48  47027  stoweidlem51  47030  stoweidlem55  47034  stoweidlem59  47038  stoweidlem60  47039  stoweidlem62  47041  fourierdlem2  47088  fourierdlem3  47089  elaa2lem  47212  etransclem11  47224  etransclem24  47237  etransclem26  47239  etransclem28  47241  etransclem35  47248  rrndistlt  47269  ioorrnopn  47284  subsaliuncllem  47336  sge0val  47345  ismea  47430  caragenval  47472  isome  47473  isomenndlem  47509  hoicvrrex  47535  ovnlecvr  47537  ovncvrrp  47543  ovn0lem  47544  ovnsubaddlem1  47549  ovnsubadd  47551  hsphoif  47555  hoidmvval  47556  hsphoival  47558  hoidmvlelem3  47576  hoidmvlelem5  47578  hoidmvle  47579  ovnhoilem1  47580  ovnhoi  47582  ovnlecvr2  47589  ovncvr2  47590  hoidifhspval2  47594  hoiqssbllem2  47602  hspmbllem2  47606  hspmbllem3  47607  hspmbl  47608  ovnovollem1  47635  smfmullem2  47771  smfmul  47774  smfpimcclem  47786  chnerlem1  47861  sqrtnnaa  47882  sqrtnzqaa  47883  sinnpoly  47910  cfsetsnfsetfv  48096  cfsetsnfsetfo  48099  iccpart  48467  iccpartiun  48485  icceuelpart  48487  nnsum3primes4  48855  nnsum3primesgbe  48859  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  bgoldbtbnd  48876  isisubgr  48929  isgrim  48949  grimidvtxedg  48952  grimcnv  48955  grimco  48956  isuspgrim0  48961  gricushgr  48984  ushggricedg  48994  uhgrimisgrgric  48998  isgrtri  49010  isubgr3stgrlem3  49035  isubgr3stgr  49042  isgrlim  49049  uspgrlim  49059  grlicref  49079  grlicsym  49080  grlictr  49082  grlimedgnedg  49198  isupwlk  49203  lincval  49490  lincdifsn  49505  linindslinci  49529  lindslinindsimp1  49538  linds0  49546  el0ldep  49547  lindsrng01  49549  snlindsntorlem  49551  ldepspr  49554  islindeps2  49564  zlmodzxzldep  49585  bigoval  49630  elbigo  49632  0aryfvalelfv  49716  1arympt1fv  49720  1arymaptfv  49721  1arymaptfo  49724  2arymptfv  49731  2arymaptfv  49732  2arymaptfo  49735  prelrrx2b  49795  rrx2plord  49801  rrx2vlinest  49822  rrx2linesl  49824  elrrx2linest2  49826  line2ylem  49832  line2xlem  49834  itsclc0  49852  itsclc0b  49853  itscnhlinecirc02p  49866  elfvne0  49928  iinfprg  50136  thincciso  50530  thinccisod  50531  setrecseq  50757  aacllem  50908  crosspval  50923  crosspdot0lem  50932  veronesevald  50940