Theorem fveq1 6834

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 5088	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6477	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6501	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6501	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2797	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5086  ℩cio 6447  ‘cfv 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501

This theorem is referenced by:  fveq1i  6836  fveq1d  6837  iffv  6852  fvmptd3f  6958  fvmptdv2  6961  eqfnun  6984  fsnex  7232  f1prex  7233  isoeq1  7266  oveq  7367  elovmpt3imp  7618  ofrfvalg  7633  offval  7634  offval3  7929  bropopvvv  8034  bropfvvvvlem  8035  poseq  8102  soseq  8103  frrlem1  8230  frrlem13  8242  smoeq  8284  tfrlem12  8322  tz7.44-2  8340  tz7.44-3  8341  rdgeq1  8344  fsetfocdm  8802  fsetprcnex  8803  mapsncnv  8835  elixp2  8843  resixpfo  8878  elixpsn  8879  mapsnend  8977  enfixsn  9018  mapxpen  9075  ac6sfi  9188  ordtypelem7  9433  wemaplem1  9455  ixpiunwdom  9499  oemapval  9598  cantnf  9608  wemapwe  9612  cnfcom3clem  9620  ssttrcl  9630  ttrcltr  9631  ttrclss  9635  ttrclselem2  9641  updjud  9852  infxpenc2lem2  9936  fseqenlem1  9940  dfac8clem  9948  ac5num  9952  acni  9961  acni2  9962  acnlem  9964  dfac4  10038  dfac5lem5  10043  dfac2a  10046  dfac9  10053  dfacacn  10058  dfac12lem1  10060  dfac12r  10063  cofsmo  10185  cfsmolem  10186  cfsmo  10187  cfcoflem  10188  coftr  10189  alephsing  10192  isfin3ds  10245  fin23lem17  10254  fin23lem32  10260  fin23lem39  10266  isf33lem  10282  isf34lem6  10296  axcc2lem  10352  axcc3  10354  axdc2lem  10364  axdc3lem2  10367  axdc3lem3  10368  axdc3  10370  axdc4lem  10371  axcclem  10373  ac6num  10395  axdclem2  10436  konigthlem  10485  inar1  10692  1fv  13595  axdc4uzlem  13939  seqeq3  13962  seqof  14015  ccatfval  14529  wrdl1s1  14571  ccat1st1st  14585  cshf1  14766  cshweqrep  14777  wrdlen2i  14898  wwlktovf  14912  wwlktovf1  14913  wwlktovfo  14914  wrd2f1tovbij  14916  rtrclreclem1  15013  dfrtrclrec2  15014  rtrclreclem2  15015  rtrclreclem4  15017  dfrtrcl2  15018  clim  15450  rlim  15451  ello1  15471  elo1  15482  summo  15673  fsum  15676  prodmo  15895  fprod  15900  bpolylem  16007  bpolyval  16008  vdwlem6  16951  vdwlem8  16953  ramcl  16994  strfvnd  17149  prdsplusgval  17430  prdsmulrval  17432  prdsleval  17434  prdsdsval  17435  prdsvscaval  17436  xpsff1o  17525  isacs2  17613  isnat  17911  yonedalem3b  18239  yonedainv  18241  ischn  18567  chnind  18581  chnub  18582  ismgmhm  18658  ismhm  18747  prdspjmhm  18791  isgrpinv  18963  pwsmulg  19089  isghm  19184  isghmOLD  19185  cayleylem2  19382  symgfix2  19385  gsmsymgrfix  19397  gsmsymgreq  19401  symgfixelq  19402  pmtr3ncomlem2  19443  pmtrdifel  19449  pmtrdifwrdel  19454  pmtrdifwrdel2  19455  psgnunilem2  19464  psgnunilem3  19465  efgsdm  19699  efgredlemd  19713  efgredlem  19716  efgred  19717  efgrelexlema  19718  efgrelexlemb  19719  prdsgsum  19950  pwspjmhmmgpd  20301  pwsexpg  20302  pwsgprod  20303  isrnghm  20415  isabv  20782  islmhm  21017  frgpcyg  21566  psgndiflemB  21593  psgndiflemA  21594  dsmmelbas  21732  frlmipval  21772  frlmphl  21774  uvcf1  21785  islindf  21805  islindf4  21831  psrmulfval  21935  evlslem2  22070  evlslem3  22071  evlslem1  22073  mpfrcl  22076  evlsvval  22081  evlsvvval  22084  selvval  22114  psdval  22138  psdcoef  22139  psdadd  22142  psdmul  22145  psdmvr  22148  coe1fval  22182  coe1mul2lem2  22246  coe1tm  22251  madetsumid  22439  mvmulval  22521  marepvval0  22544  mulmarep1gsum2  22552  mdetleib2  22566  m1detdiag  22575  mdetralt  22586  mdetunilem7  22596  mdetunilem9  22598  m2detleiblem3  22607  m2detleiblem4  22608  m2detleib  22609  symgmatr01lem  22631  gsummatr01lem1  22633  gsummatr01lem4  22636  gsummatr01  22637  smadiadetlem3  22646  pmatcoe1fsupp  22679  pmatcollpw3lem  22761  pmatcollpw3fi1lem2  22765  iscnp  23215  1stcfb  23423  ptpjpre1  23549  elpt  23550  elptr  23551  ptpjopn  23590  dfac14  23596  upxp  23601  pthaus  23616  ptrescn  23617  xkoptsub  23632  cnmptkp  23658  xkofvcn  23662  cnmptk1p  23663  cnmptk2  23664  ptunhmeo  23786  ptcmplem3  24032  ptcmplem4  24033  symgtgp  24084  prdstmdd  24102  isucn  24255  imasdsf1olem  24351  prdsxmslem2  24507  tngngp3  24634  nmoval  24693  elcncf  24869  ishtpy  24952  pcoval  24991  om1elbas  25012  elpi1i  25026  iscau  25256  rrxds  25373  rrxdsfival  25393  ehl1eudisval  25401  ehl2eudisval  25403  mbfi1fseqlem6  25700  mbfi1flimlem  25702  isibl  25745  deg1ldg  26070  deg1leb  26073  elply2  26174  elplyr  26179  ne0p  26185  coeeu  26203  coelem  26204  coeeq  26205  coeidlem  26215  elqaalem3  26301  qaa  26303  iaa  26305  aareccl  26306  aannenlem2  26309  aaliou2  26320  dchrptlem2  27245  dchrpt  27247  dchrsum2  27248  sumdchr2  27250  dchrvmaeq0  27484  rpvmasum2  27492  dchrisum0re  27493  ostth  27619  ltsval  27628  nolesgn2o  27652  nogesgn1o  27654  noresle  27678  nosupprefixmo  27681  noinfprefixmo  27682  nosupcbv  27683  nosupfv  27687  noinfcbv  27698  noinffv  27702  iscgrg  28597  isismt  28619  israg  28782  iseqlg  28952  brbtwn  28985  brbtwn2  28991  colinearalg  28996  axsegconlem1  29003  axsegcon  29013  ax5seglem5  29019  axpasch  29027  axlowdim  29047  axeuclidlem  29048  axcontlem1  29050  axcontlem2  29051  axcontlem5  29054  vtxdgfval  29554  1egrvtxdg1  29596  isewlk  29689  iswlk  29697  uspgr2wlkeq2  29733  iswlkon  29742  isclwlk  29859  iscrct  29876  iscycl  29877  iswwlks  29922  wwlknon  29943  wlkiswwlks2  29961  wwlksnredwwlkn0  29982  wlksnwwlknvbij  29994  wwlksnextproplem3  29997  wwlksnextprop  29998  umgr2wlk  30035  midwwlks2s3  30038  elwwlks2  30055  elwspths2spth  30056  rusgrnumwwlkslem  30058  rusgrnumwwlkb0  30060  rusgrnumwwlks  30063  isclwwlk  30072  clwlkclwwlklem1  30087  clwwlkn1loopb  30131  clwwlkel  30134  clwwlkf  30135  clwwlkf1  30137  isclwwlknon  30179  clwwlknon1  30185  s2elclwwlknon2  30192  clwwlkvbij  30201  uhgr3cyclex  30270  fusgreg2wsplem  30421  fusgr2wsp2nb  30422  fusgreghash2wsp  30426  2clwwlkel  30437  extwwlkfabel  30441  numclwwlk1lem2fv  30444  numclwwlk1lem2  30448  clwwlknonclwlknonf1o  30450  dlwwlknondlwlknonf1o  30453  numclwwlk2lem1  30464  numclwlk2lem2f  30465  numclwlk2lem2f1o  30467  ex-fv  30531  isnvlem  30699  islno  30842  nmooval  30852  nmblolbi  30889  isphg  30906  ajmoi  30947  ajval  30950  ubthlem3  30961  htthlem  31006  hcau  31273  hlimi  31277  hosmval  31824  hommval  31825  hodmval  31826  hfsmval  31827  hfmmval  31828  adjmo  31921  nmopval  31945  elcnop  31946  ellnop  31947  elunop  31961  elhmop  31962  nmfnval  31965  elcnfn  31971  ellnfn  31972  adjeu  31978  adjval  31979  eigvecval  31985  eigvalfval  31986  adj1  32022  adjeq  32024  hmopadj2  32030  lnopeq0i  32096  lnopeq  32098  elunop2  32102  lnophm  32108  hmopco  32112  nmbdoplb  32114  nmcoplb  32119  lnopcon  32124  lnfn0  32136  lnfnmul  32137  nmbdfnlb  32139  nmcfnlb  32143  lnfncon  32145  riesz4  32153  riesz1  32154  cnlnadjlem9  32164  cnlnadjeu  32167  cnlnssadj  32169  nmopcoi  32184  bra11  32197  cnvbraval  32199  pjss2coi  32253  pjssdif2i  32263  pjssdif1i  32264  pjclem4  32288  pj3si  32296  pj3cor1i  32298  isst  32302  ishst  32303  stri  32346  hstri  32354  aciunf1lem  32753  ismnt  33061  mgcval  33065  fzo0pmtrlast  33171  elrgspnlem1  33321  elrgspnlem2  33322  elrgspnlem3  33323  elrgspnlem4  33324  elrgspn  33325  elrgspnsubrunlem1  33326  linds2eq  33459  elrspunidl  33506  elrspunsn  33507  dfufd2lem  33627  extvfv  33695  extvfvv  33696  extvfvcl  33698  evlvarval  33703  evlextv  33704  mplvrpmga  33707  splysubrg  33722  issply  33723  vietalem  33741  vieta  33742  lbsdiflsp0  33789  fedgmullem1  33792  fedgmullem2  33793  fedgmul  33794  fldextrspunlsplem  33836  fldextrspunlsp  33837  fldext2chn  33891  constrextdg2lem  33911  constrextdg2  33912  lmatval  33976  mdetpmtr1  33986  zarcmplem  34044  ismeas  34362  isrnmeas  34363  cntnevol  34391  carsgval  34466  sitgval  34495  eulerpartleme  34526  eulerpartlemd  34529  eulerpartlemr  34537  eulerpartlemgvv  34539  eulerpart  34545  cndprobval  34596  signstfvneq0  34735  reprsum  34776  reprsuc  34778  reprpmtf1o  34789  reprdifc  34790  breprexp  34796  vtsval  34800  hgt750lemb  34819  hgt750lema  34820  hgt750leme  34821  bnj66  35021  bnj106  35029  bnj125  35033  bnj154  35039  bnj155  35040  bnj526  35049  bnj540  35053  bnj609  35078  bnj611  35079  bnj893  35089  bnj1000  35102  bnj1014  35122  bnj1015  35123  bnj1234  35174  bnj1463  35216  fineqvnttrclse  35287  gblacfnacd  35303  loop1cycl  35338  derangenlem  35372  subfacp1lem3  35383  subfacp1lem5  35385  subfacp1lem6  35386  subfacp1  35387  sconnpht  35430  cnpconn  35431  txpconn  35433  ptpconn  35434  indispconn  35435  connpconn  35436  cvxpconn  35443  cvmliftmo  35485  cvmliftlem14  35498  cvmliftlem15  35499  cvmliftiota  35502  cvmlift2  35517  cvmliftphtlem  35518  cvmlift3lem2  35521  cvmlift3lem6  35525  cvmlift3lem7  35526  cvmlift3lem9  35528  cvmlift3  35529  satfv1lem  35563  satfv1  35564  sategoelfvb  35620  mrsubff1  35715  mrsub0  35717  mrsubccat  35719  mrsubcn  35720  elmsubrn  35729  msubrn  35730  msubco  35732  msubvrs  35761  mclsax  35770  shftvalg  35933  fwddifval  36363  fwddifnval  36364  bj-evalval  37406  unceq  37935  matunitlindflem2  37955  poimirlem17  37975  poimirlem20  37978  poimirlem22  37980  poimirlem23  37981  poimirlem27  37985  poimirlem28  37986  poimirlem30  37988  poimirlem31  37989  poimirlem32  37990  poimir  37991  broucube  37992  voliunnfl  38002  volsupnfl  38003  itg2addnclem  38009  itg2addnclem3  38011  itg2addnc  38012  ftc1anclem2  38032  ftc1anclem5  38035  upixp  38067  fdc  38083  isismty  38139  rrnmval  38166  elghomlem2OLD  38224  isrngohom  38303  islfl  39523  isopos  39643  islaut  40546  ispautN  40562  isldil  40573  isltrn  40582  ltrnid  40598  ltrneq2  40611  isdilN  40617  istrnN  40620  trlval  40625  ltrneq3  40671  cdleme50ex  41022  cdleme  41023  cdlemg1a  41033  ltrniotaval  41044  ltrniotavalbN  41047  cdlemeiota  41048  cdlemg2jlemOLDN  41056  cdlemg2fvlem  41057  cdlemg2klem  41058  istendo  41223  tendoplcbv  41238  tendopl  41239  tendoicbv  41256  tendoi  41257  tendoid0  41288  tendo1ne0  41291  cdlemksv2  41310  cdlemkuv2  41330  cdlemk33N  41372  cdlemk34  41373  cdlemk36  41376  cdlemk19u  41433  cdlemk  41437  tendoex  41438  dvavsca  41480  dvhvscacbv  41561  dvhvscaval  41562  dicopelval  41640  dicelval1sta  41650  diclspsn  41657  dihmeetlem13N  41782  dih1dimatlem0  41791  dih1dimatlem  41792  dihpN  41799  islpolN  41946  hdmap1fval  42259  hdmapfval  42290  sticksstones1  42602  sticksstones2  42603  sticksstones3  42604  sticksstones8  42609  sticksstones10  42611  sticksstones11  42612  sticksstones12a  42613  sticksstones12  42614  sticksstones15  42617  frlmsnic  43002  uvcn0  43004  mplmapghm  43014  evlsvarval  43018  evlsbagval  43019  selvvvval  43035  evlselv  43037  fsuppssindlem2  43042  fsuppssind  43043  prjspnfv01  43074  prjspner01  43075  prjspner1  43076  sn-isghm  43123  ismrc  43150  mzpclval  43174  mzpsubst  43197  mzprename  43198  mzpcompact2lem  43200  eldioph  43207  eldioph2  43211  eldioph2b  43212  eldioph3  43215  rexrabdioph  43243  2rexfrabdioph  43245  3rexfrabdioph  43246  4rexfrabdioph  43247  6rexfrabdioph  43248  7rexfrabdioph  43249  eldioph4i  43261  rabren3dioph  43264  mzpcong  43421  jm2.27dlem1  43458  wepwsolem  43491  aomclem6  43508  aomclem8  43510  dfac11  43511  dgraalem  43594  dgraaub  43597  dgraa0p  43598  mpaaeu  43599  mpaalem  43601  aaitgo  43611  rngunsnply  43618  cantnfresb  43773  tfsconcatun  43786  nvocnvb  43870  eliunov2  44127  rfovcnvfvd  44455  fsovfvd  44458  fsovcnvlem  44461  dssmapfv2d  44466  dssmapnvod  44468  clsk1independent  44494  ntrclskb  44517  ntrclsk13  44519  gneispace2  44580  mnringmulrvald  44675  dvconstbi  44782  addrval  44913  subrval  44914  mulvval  44915  relpeq1  45392  fnchoice  45481  refsum2cnlem1  45489  choicefi  45650  axccdom  45672  fmulcl  46032  fmuldfeqlem1  46033  mccllem  46048  mccl  46049  climf  46073  climf2  46115  dvnprodlem1  46395  dvnprodlem3  46397  dvnprod  46398  stoweidlem2  46451  stoweidlem6  46455  stoweidlem8  46457  stoweidlem9  46458  stoweidlem15  46464  stoweidlem16  46465  stoweidlem17  46466  stoweidlem18  46467  stoweidlem21  46470  stoweidlem27  46476  stoweidlem31  46480  stoweidlem36  46485  stoweidlem37  46486  stoweidlem41  46490  stoweidlem43  46492  stoweidlem44  46493  stoweidlem45  46494  stoweidlem46  46495  stoweidlem48  46497  stoweidlem51  46500  stoweidlem55  46504  stoweidlem59  46508  stoweidlem60  46509  stoweidlem62  46511  fourierdlem2  46558  fourierdlem3  46559  elaa2lem  46682  etransclem11  46694  etransclem24  46707  etransclem26  46709  etransclem28  46711  etransclem35  46718  rrndistlt  46739  ioorrnopn  46754  subsaliuncllem  46806  sge0val  46815  ismea  46900  caragenval  46942  isome  46943  isomenndlem  46979  hoicvrrex  47005  ovnlecvr  47007  ovncvrrp  47013  ovn0lem  47014  ovnsubaddlem1  47019  ovnsubadd  47021  hsphoif  47025  hoidmvval  47026  hsphoival  47028  hoidmvlelem3  47046  hoidmvlelem5  47048  hoidmvle  47049  ovnhoilem1  47050  ovnhoi  47052  ovnlecvr2  47059  ovncvr2  47060  hoidifhspval2  47064  hoiqssbllem2  47072  hspmbllem2  47076  hspmbllem3  47077  hspmbl  47078  ovnovollem1  47105  smfmullem2  47241  smfmul  47244  smfpimcclem  47256  chnerlem1  47331  nthrucw  47335  sinnpoly  47354  cfsetsnfsetfv  47520  cfsetsnfsetfo  47523  iccpart  47891  iccpartiun  47909  icceuelpart  47911  nnsum3primes4  48279  nnsum3primesgbe  48283  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  bgoldbtbnd  48300  isisubgr  48353  isgrim  48373  grimidvtxedg  48376  grimcnv  48379  grimco  48380  isuspgrim0  48385  gricushgr  48408  ushggricedg  48418  uhgrimisgrgric  48422  isgrtri  48434  isubgr3stgrlem3  48459  isubgr3stgr  48466  isgrlim  48473  uspgrlim  48483  grlicref  48503  grlicsym  48504  grlictr  48506  grlimedgnedg  48622  isupwlk  48627  lincval  48900  lincdifsn  48915  linindslinci  48939  lindslinindsimp1  48948  linds0  48956  el0ldep  48957  lindsrng01  48959  snlindsntorlem  48961  ldepspr  48964  islindeps2  48974  zlmodzxzldep  48995  bigoval  49040  elbigo  49042  0aryfvalelfv  49126  1arympt1fv  49130  1arymaptfv  49131  1arymaptfo  49134  2arymptfv  49141  2arymaptfv  49142  2arymaptfo  49145  prelrrx2b  49205  rrx2plord  49211  rrx2vlinest  49232  rrx2linesl  49234  elrrx2linest2  49236  line2ylem  49242  line2xlem  49244  itsclc0  49262  itsclc0b  49263  itscnhlinecirc02p  49276  elfvne0  49339  iinfprg  49549  thincciso  49943  thinccisod  49944  setrecseq  50175  aacllem  50291