Theorem fveq1 6884

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 5113	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6524	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6548	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6548	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2825	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5111  ℩cio 6494  ‘cfv 6540

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548

This theorem is used by:  fveq1i  6886  fveq1d  6887  iffv  6902  fvmptd3f  7009  fvmptdv2  7012  eqfnun  7036  fsnex  7290  f1prex  7291  isoeq1  7324  oveq  7425  elovmpt3imp  7677  ofrfvalg  7692  offval  7693  offval3  7985  bropopvvv  8091  bropfvvvvlem  8092  poseq  8160  soseq  8161  frrlem1  8289  frrlem13  8301  smoeq  8343  tfrlem12  8382  tz7.44-2  8400  tz7.44-3  8401  rdgeq1  8404  fsetfocdm  8864  fsetprcnex  8865  mapsncnv  8897  elixp2  8905  resixpfo  8940  elixpsn  8941  mapsnend  9040  enfixsn  9081  mapxpen  9138  ac6sfi  9251  ordtypelem7  9493  wemaplem1  9515  ixpiunwdom  9559  oemapval  9659  cantnf  9669  wemapwe  9673  cnfcom3clem  9681  ssttrcl  9691  ttrcltr  9692  ttrclss  9696  ttrclselem2  9702  updjud  9936  infxpenc2lem2  10020  fseqenlem1  10024  dfac8clem  10032  ac5num  10036  acni  10045  acni2  10046  acnlem  10048  dfac4  10122  dfac5lem5  10127  dfac2a  10129  dfac9  10136  dfacacn  10141  dfac12lem1  10143  dfac12r  10146  cofsmo  10268  cfsmolem  10269  cfsmo  10270  cfcoflem  10271  coftr  10272  alephsing  10275  isfin3ds  10328  fin23lem17  10337  fin23lem32  10343  fin23lem39  10349  isf33lem  10365  isf34lem6  10379  axcc2lem  10435  axcc3  10437  axdc2lem  10447  axdc3lem2  10450  axdc3lem3  10451  axdc3  10453  axdc4lem  10454  axcclem  10456  ac6num  10478  axdclem2  10519  konigthlem  10568  inar1  10775  1fv  13692  axdc4uzlem  14037  seqeq3  14060  seqof  14113  ccatfval  14628  wrdl1s1  14672  ccat1st1st  14686  cshf1  14871  cshweqrep  14882  wrdlen2i  15003  wwlktovf  15017  wwlktovf1  15018  wwlktovfo  15019  wrd2f1tovbij  15021  rtrclreclem1  15118  dfrtrclrec2  15119  rtrclreclem2  15120  rtrclreclem4  15122  dfrtrcl2  15123  clim  15569  rlim  15570  ello1  15590  elo1  15601  summo  15791  fsum  15794  prodmo  16013  fprod  16018  bpolylem  16124  bpolyval  16125  vdwlem6  17068  vdwlem8  17070  ramcl  17111  strfvnd  17267  prdsplusgval  17548  prdsmulrval  17550  prdsleval  17552  prdsdsval  17553  prdsvscaval  17554  xpsff1o  17643  isacs2  17731  isnat  18029  yonedalem3b  18357  yonedainv  18359  ischn  18685  chnind  18699  chnub  18700  ismgmhm  18786  ismhm  18880  prdspjmhm  18925  isgrpinv  19104  pwsmulg  19229  isghm  19330  cayleylem2  19527  symgfix2  19530  gsmsymgrfix  19542  gsmsymgreq  19546  symgfixelq  19547  pmtr3ncomlem2  19588  pmtrdifel  19594  pmtrdifwrdel  19599  pmtrdifwrdel2  19600  psgnunilem2  19609  psgnunilem3  19610  efgsdm  19844  efgredlemd  19858  efgredlem  19861  efgred  19862  efgrelexlema  19863  efgrelexlemb  19864  prdsgsum  20095  pwspjmhmmgpd  20455  pwsexpg  20456  pwsgprod  20457  isrnghm  20569  isrhm0  20604  isabv  20964  islmhm  21198  frgpcyg  21773  psgndiflemB  21800  psgndiflemA  21801  dsmmelbas  21939  frlmipval  21979  frlmphl  21981  uvcf1  21992  islindf  22012  islindf4  22038  psrmulfval  22143  evlslem2  22280  evlslem3  22281  evlslem1  22283  mpfrcl  22286  evlsvval  22291  evlsvvval  22294  selvval  22321  mplmapghm  22323  evlsvarval  22328  selvvvval  22343  psdval  22372  psdcoef  22373  psdadd  22376  psdmul  22379  psdmvr  22382  coe1fval  22415  coe1mul2lem2  22479  coe1tm  22484  madetsumid  22668  mvmulval  22750  marepvval0  22773  mulmarep1gsum2  22781  mdetleib2  22795  m1detdiag  22804  mdetralt  22815  mdetunilem7  22825  mdetunilem9  22827  m2detleiblem3  22836  m2detleiblem4  22837  m2detleib  22838  symgmatr01lem  22860  gsummatr01lem1  22862  gsummatr01lem4  22865  gsummatr01  22866  smadiadetlem3  22875  pmatcoe1fsupp  22908  pmatcollpw3lem  22990  pmatcollpw3fi1lem2  22994  iscnp  23444  1stcfb  23652  ptpjpre1  23779  elpt  23780  elptr  23781  ptpjopn  23820  dfac14  23826  upxp  23831  pthaus  23846  ptrescn  23847  xkoptsub  23862  cnmptkp  23888  xkofvcn  23892  cnmptk1p  23893  cnmptk2  23894  ptunhmeo  24016  ptcmplem3  24262  ptcmplem4  24263  symgtgp  24314  prdstmdd  24332  isucn  24485  imasdsf1olem  24581  prdsxmslem2  24737  tngngp3  24864  nmoval  24923  elcncf  25099  ishtpy  25182  pcoval  25221  om1elbas  25242  elpi1i  25256  iscau  25486  rrxds  25603  rrxdsfival  25623  ehl1eudisval  25631  ehl2eudisval  25633  mbfi1fseqlem6  25930  mbfi1flimlem  25932  isibl  25975  deg1ldg  26300  deg1leb  26303  elply2  26404  elplyr  26409  ne0p  26415  coeeu  26433  coelem  26434  coeeq  26435  coeidlem  26445  elqaalem3  26533  qaa  26535  iaa  26539  aareccl  26540  aannenlem2  26543  aaliou2  26554  dchrptlem2  27480  dchrpt  27482  dchrsum2  27483  sumdchr2  27485  dchrvmaeq0  27719  rpvmasum2  27727  dchrisum0re  27728  ostth  27854  ltsval  27862  nolesgn2o  27886  nogesgn1o  27888  noresle  27912  nosupprefixmo  27915  noinfprefixmo  27916  nosupcbv  27917  nosupfv  27921  noinfcbv  27932  noinffv  27936  iscgrg  28832  isismt  28854  israg  29028  iseqlg  29239  brbtwn  29304  brbtwn2  29310  colinearalg  29315  axsegconlem1  29322  axsegcon  29332  ax5seglem5  29338  axpasch  29346  axlowdim  29366  axeuclidlem  29367  axcontlem1  29369  axcontlem2  29370  axcontlem5  29373  vtxdgfval  29875  1egrvtxdg1  29917  isewlk  30010  iswlk  30018  uspgr2wlkeq2  30054  iswlkon  30063  isclwlk  30187  iscrct  30204  iscycl  30205  iswwlks  30252  wwlknon  30273  wlkiswwlks2  30291  wwlksnredwwlkn0  30312  wlksnwwlknvbij  30324  wwlksnextproplem3  30327  wwlksnextprop  30328  umgr2wlk  30365  midwwlks2s3  30368  elwwlks2  30385  elwspths2spth  30386  rusgrnumwwlkslem  30388  rusgrnumwwlkb0  30390  rusgrnumwwlks  30393  isclwwlk  30402  clwlkclwwlklem1  30417  clwwlkn1loopb  30461  clwwlkel  30464  clwwlkf  30465  clwwlkf1  30467  isclwwlknon  30509  clwwlknon1  30515  s2elclwwlknon2  30522  clwwlkvbij  30531  loop1cycl  30571  uhgr3cyclex  30604  fusgreg2wsplem  30755  fusgr2wsp2nb  30756  fusgreghash2wsp  30760  2clwwlkel  30771  extwwlkfabel  30775  numclwwlk1lem2fv  30778  numclwwlk1lem2  30782  clwwlknonclwlknonf1o  30784  dlwwlknondlwlknonf1o  30787  numclwwlk2lem1  30798  numclwlk2lem2f  30799  numclwlk2lem2f1o  30801  ex-fv  30865  isnvlem  31033  islno  31176  nmooval  31186  nmblolbi  31223  isphg  31240  ajmoi  31281  ajval  31284  ubthlem3  31295  htthlem  31340  hcau  31607  hlimi  31611  hosmval  32158  hommval  32159  hodmval  32160  hfsmval  32161  hfmmval  32162  adjmo  32255  nmopval  32279  elcnop  32280  ellnop  32281  elunop  32295  elhmop  32296  nmfnval  32299  elcnfn  32305  ellnfn  32306  adjeu  32312  adjval  32313  eigvecval  32319  eigvalfval  32320  adj1  32356  adjeq  32358  hmopadj2  32364  lnopeq0i  32430  lnopeq  32432  elunop2  32436  lnophm  32442  hmopco  32446  nmbdoplb  32448  nmcoplb  32453  lnopcon  32458  lnfn0  32470  lnfnmul  32471  nmbdfnlb  32473  nmcfnlb  32477  lnfncon  32479  riesz4  32487  riesz1  32488  cnlnadjlem9  32498  cnlnadjeu  32501  cnlnssadj  32503  nmopcoi  32518  bra11  32531  cnvbraval  32533  pjss2coi  32587  pjssdif2i  32597  pjssdif1i  32598  pjclem4  32622  pj3si  32630  pj3cor1i  32632  isst  32636  ishst  32637  stri  32680  hstri  32688  aciunf1lem  33078  ismnt  33367  mgcval  33371  fzo0pmtrlast  33476  elrgspnlem1  33626  elrgspnlem2  33627  elrgspnlem3  33628  elrgspnlem4  33629  elrgspn  33630  elrgspnsubrunlem1  33631  linds2eq  33758  elrspunidl  33800  elrspunsn  33801  dfufd2lem  33903  psrnzr  33966  0mplrim  33968  0mplric  33969  selvply1rhmlema  33972  selvply1rhmlemb  33973  selvply1rhmlem1  33974  selvply1rhmlem3  33976  selvply1rhmlem5  33978  selvply1rhm  33979  mplidom  33982  extvfv  33987  extvfvv  33988  extvfvcl  33990  evlvarval  33995  evlextv  33996  mplvrpmga  33999  splysubrg  34014  issply  34015  vietalem  34033  vieta  34034  lbsdiflsp0  34080  fedgmullem1  34083  fedgmullem2  34084  fedgmul  34085  fldextrspunlsplem  34127  fldextrspunlsp  34128  fldext2chn  34182  constrextdg2lem  34202  constrextdg2  34203  lmatval  34267  mdetpmtr1  34277  zarcmplem  34335  ismeas  34654  isrnmeas  34655  cntnevol  34683  carsgval  34758  sitgval  34787  eulerpartleme  34818  eulerpartlemd  34821  eulerpartlemr  34829  eulerpartlemgvv  34831  eulerpart  34837  cndprobval  34888  signstfvneq0  35024  reprsum  35065  reprsuc  35067  reprpmtf1o  35078  reprdifc  35079  breprexp  35085  vtsval  35089  hgt750lemb  35108  hgt750lema  35109  hgt750leme  35110  bnj66  35313  bnj106  35321  bnj125  35325  bnj154  35331  bnj155  35332  bnj526  35341  bnj540  35345  bnj609  35370  bnj611  35371  bnj893  35381  bnj1000  35394  bnj1014  35414  bnj1015  35415  bnj1234  35466  bnj1463  35508  fineqvnttrclse  35594  gblacfnacd  35643  derangenlem  35700  subfacp1lem3  35711  subfacp1lem5  35713  subfacp1lem6  35714  subfacp1  35715  sconnpht  35758  cnpconn  35759  txpconn  35761  ptpconn  35762  indispconn  35763  connpconn  35764  cvxpconn  35771  cvmliftmo  35813  cvmliftlem14  35826  cvmliftlem15  35827  cvmliftiota  35830  cvmlift2  35845  cvmliftphtlem  35846  cvmlift3lem2  35849  cvmlift3lem6  35853  cvmlift3lem7  35854  cvmlift3lem9  35856  cvmlift3  35857  satfv1lem  35891  satfv1  35892  sategoelfvb  35948  mrsubff1  36043  mrsub0  36045  mrsubccat  36047  mrsubcn  36048  elmsubrn  36057  msubrn  36058  msubco  36060  msubvrs  36089  mclsax  36098  shftvalg  36261  fwddifval  36691  fwddifnval  36692  bj-evalval  37774  unceq  38305  matunitlindflem2  38325  poimirlem17  38345  poimirlem20  38348  poimirlem22  38350  poimirlem23  38351  poimirlem27  38355  poimirlem28  38356  poimirlem30  38358  poimirlem31  38359  poimirlem32  38360  poimir  38361  broucube  38362  voliunnfl  38372  volsupnfl  38373  itg2addnclem  38379  itg2addnclem3  38381  itg2addnc  38382  ftc1anclem2  38402  ftc1anclem5  38405  upixp  38438  fdc  38454  isismty  38510  rrnmval  38537  elghomlem2OLD  38595  isrngohom  38674  islfl  39892  isopos  40012  islaut  40915  ispautN  40931  isldil  40942  isltrn  40951  ltrnid  40967  ltrneq2  40980  isdilN  40986  istrnN  40989  trlval  40994  ltrneq3  41040  cdleme50ex  41391  cdleme  41392  cdlemg1a  41402  ltrniotaval  41413  ltrniotavalbN  41416  cdlemeiota  41417  cdlemg2jlemOLDN  41425  cdlemg2fvlem  41426  cdlemg2klem  41427  istendo  41592  tendoplcbv  41607  tendopl  41608  tendoicbv  41625  tendoi  41626  tendoid0  41657  tendo1ne0  41660  cdlemksv2  41679  cdlemkuv2  41699  cdlemk33N  41741  cdlemk34  41742  cdlemk36  41745  cdlemk19u  41802  cdlemk  41806  tendoex  41807  dvavsca  41849  dvhvscacbv  41930  dvhvscaval  41931  dicopelval  42009  dicelval1sta  42019  diclspsn  42026  dihmeetlem13N  42151  dih1dimatlem0  42160  dih1dimatlem  42161  dihpN  42168  islpolN  42315  hdmap1fval  42628  hdmapfval  42659  sticksstones1  42971  sticksstones2  42972  sticksstones3  42973  sticksstones8  42978  sticksstones10  42980  sticksstones11  42981  sticksstones12a  42982  sticksstones12  42983  sticksstones15  42986  frlmsnic  43366  uvcn0  43368  evlsbagval  43376  evlselv  43379  fsuppssindlem2  43382  fsuppssind  43383  prjspnfv01  43414  prjspner01  43415  prjspner1  43416  sn-isghm  43463  ismrc  43490  mzpclval  43514  mzpsubst  43537  mzprename  43538  mzpcompact2lem  43540  eldioph  43547  eldioph2  43551  eldioph2b  43552  eldioph3  43555  rexrabdioph  43579  2rexfrabdioph  43581  3rexfrabdioph  43582  4rexfrabdioph  43583  6rexfrabdioph  43584  7rexfrabdioph  43585  eldioph4i  43597  rabren3dioph  43600  mzpcong  43757  jm2.27dlem1  43794  wepwsolem  43827  aomclem6  43844  aomclem8  43846  dfac11  43847  dgraalem  43930  dgraaub  43933  dgraa0p  43934  mpaaeu  43935  mpaalem  43937  aaitgo  43947  rngunsnply  43954  cantnfresb  44109  tfsconcatun  44122  nvocnvb  44206  eliunov2  44463  rfovcnvfvd  44791  fsovfvd  44794  fsovcnvlem  44797  dssmapfv2d  44802  dssmapnvod  44804  clsk1independent  44830  ntrclskb  44853  ntrclsk13  44855  gneispace2  44916  mnringmulrvald  45009  dvconstbi  45102  addrval  45232  subrval  45233  mulvval  45234  relpeq1  45711  fnchoice  45807  refsum2cnlem1  45815  choicefi  45975  axccdom  45996  fmulcl  46355  fmuldfeqlem1  46356  mccllem  46371  mccl  46372  climf  46396  climf2  46438  dvnprodlem1  46718  dvnprodlem3  46720  dvnprod  46721  stoweidlem2  46774  stoweidlem6  46778  stoweidlem8  46780  stoweidlem9  46781  stoweidlem15  46787  stoweidlem16  46788  stoweidlem17  46789  stoweidlem18  46790  stoweidlem21  46793  stoweidlem27  46799  stoweidlem31  46803  stoweidlem36  46808  stoweidlem37  46809  stoweidlem41  46813  stoweidlem43  46815  stoweidlem44  46816  stoweidlem45  46817  stoweidlem46  46818  stoweidlem48  46820  stoweidlem51  46823  stoweidlem55  46827  stoweidlem59  46831  stoweidlem60  46832  stoweidlem62  46834  fourierdlem2  46881  fourierdlem3  46882  elaa2lem  47005  etransclem11  47017  etransclem24  47030  etransclem26  47032  etransclem28  47034  etransclem35  47041  rrndistlt  47062  ioorrnopn  47077  subsaliuncllem  47129  sge0val  47138  ismea  47223  caragenval  47265  isome  47266  isomenndlem  47302  hoicvrrex  47328  ovnlecvr  47330  ovncvrrp  47336  ovn0lem  47337  ovnsubaddlem1  47342  ovnsubadd  47344  hsphoif  47348  hoidmvval  47349  hsphoival  47351  hoidmvlelem3  47369  hoidmvlelem5  47371  hoidmvle  47372  ovnhoilem1  47373  ovnhoi  47375  ovnlecvr2  47382  ovncvr2  47383  hoidifhspval2  47387  hoiqssbllem2  47395  hspmbllem2  47399  hspmbllem3  47400  hspmbl  47401  ovnovollem1  47428  smfmullem2  47564  smfmul  47567  smfpimcclem  47579  chnerlem1  47656  sqrtnnaa  47662  sqrtnzqaa  47663  sinnpoly  47686  cfsetsnfsetfv  47852  cfsetsnfsetfo  47855  iccpart  48223  iccpartiun  48241  icceuelpart  48243  nnsum3primes4  48611  nnsum3primesgbe  48615  nnsum4primesodd  48619  nnsum4primesoddALTV  48620  nnsum4primeseven  48623  nnsum4primesevenALTV  48624  bgoldbtbnd  48632  isisubgr  48685  isgrim  48705  grimidvtxedg  48708  grimcnv  48711  grimco  48712  isuspgrim0  48717  gricushgr  48740  ushggricedg  48750  uhgrimisgrgric  48754  isgrtri  48766  isubgr3stgrlem3  48791  isubgr3stgr  48798  isgrlim  48805  uspgrlim  48815  grlicref  48835  grlicsym  48836  grlictr  48838  grlimedgnedg  48954  isupwlk  48959  lincval  49246  lincdifsn  49261  linindslinci  49285  lindslinindsimp1  49294  linds0  49302  el0ldep  49303  lindsrng01  49305  snlindsntorlem  49307  ldepspr  49310  islindeps2  49320  zlmodzxzldep  49341  bigoval  49386  elbigo  49388  0aryfvalelfv  49472  1arympt1fv  49476  1arymaptfv  49477  1arymaptfo  49480  2arymptfv  49487  2arymaptfv  49488  2arymaptfo  49491  prelrrx2b  49551  rrx2plord  49557  rrx2vlinest  49578  rrx2linesl  49580  elrrx2linest2  49582  line2ylem  49588  line2xlem  49590  itsclc0  49608  itsclc0b  49609  itscnhlinecirc02p  49622  elfvne0  49684  iinfprg  49894  thincciso  50288  thinccisod  50289  setrecseq  50520  aacllem  50678  crosspval  50693  crosspdot0lem  50702