Theorem fveq1 6821

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 5091	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6465	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6489	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6489	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2791	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5089  ℩cio 6435  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489

This theorem is referenced by:  fveq1i  6823  fveq1d  6824  iffv  6839  fvmptd3f  6944  fvmptdv2  6947  eqfnun  6970  fsnex  7217  f1prex  7218  isoeq1  7251  oveq  7352  elovmpt3imp  7603  ofrfvalg  7618  offval  7619  offval3  7914  bropopvvv  8020  bropfvvvvlem  8021  poseq  8088  soseq  8089  frrlem1  8216  frrlem13  8228  smoeq  8270  tfrlem12  8308  tz7.44-2  8326  tz7.44-3  8327  rdgeq1  8330  fsetfocdm  8785  fsetprcnex  8786  mapsncnv  8817  elixp2  8825  resixpfo  8860  elixpsn  8861  mapsnend  8958  enfixsn  8999  mapxpen  9056  ac6sfi  9168  ordtypelem7  9410  wemaplem1  9432  ixpiunwdom  9476  oemapval  9573  cantnf  9583  wemapwe  9587  cnfcom3clem  9595  ssttrcl  9605  ttrcltr  9606  ttrclss  9610  ttrclselem2  9616  updjud  9827  infxpenc2lem2  9911  fseqenlem1  9915  dfac8clem  9923  ac5num  9927  acni  9936  acni2  9937  acnlem  9939  dfac4  10013  dfac5lem5  10018  dfac2a  10021  dfac9  10028  dfacacn  10033  dfac12lem1  10035  dfac12r  10038  cofsmo  10160  cfsmolem  10161  cfsmo  10162  cfcoflem  10163  coftr  10164  alephsing  10167  isfin3ds  10220  fin23lem17  10229  fin23lem32  10235  fin23lem39  10241  isf33lem  10257  isf34lem6  10271  axcc2lem  10327  axcc3  10329  axdc2lem  10339  axdc3lem2  10342  axdc3lem3  10343  axdc3  10345  axdc4lem  10346  axcclem  10348  ac6num  10370  axdclem2  10411  konigthlem  10459  inar1  10666  1fv  13547  axdc4uzlem  13890  seqeq3  13913  seqof  13966  ccatfval  14480  wrdl1s1  14522  ccat1st1st  14536  cshf1  14717  cshweqrep  14728  wrdlen2i  14849  wwlktovf  14863  wwlktovf1  14864  wwlktovfo  14865  wrd2f1tovbij  14867  rtrclreclem1  14964  dfrtrclrec2  14965  rtrclreclem2  14966  rtrclreclem4  14968  dfrtrcl2  14969  clim  15401  rlim  15402  ello1  15422  elo1  15433  summo  15624  fsum  15627  prodmo  15843  fprod  15848  bpolylem  15955  bpolyval  15956  vdwlem6  16898  vdwlem8  16900  ramcl  16941  strfvnd  17096  prdsplusgval  17377  prdsmulrval  17379  prdsleval  17381  prdsdsval  17382  prdsvscaval  17383  xpsff1o  17471  isacs2  17559  isnat  17857  yonedalem3b  18185  yonedainv  18187  ischn  18513  chnind  18527  chnub  18528  ismgmhm  18604  ismhm  18693  prdspjmhm  18737  isgrpinv  18906  pwsmulg  19032  isghm  19127  isghmOLD  19128  cayleylem2  19325  symgfix2  19328  gsmsymgrfix  19340  gsmsymgreq  19344  symgfixelq  19345  pmtr3ncomlem2  19386  pmtrdifel  19392  pmtrdifwrdel  19397  pmtrdifwrdel2  19398  psgnunilem2  19407  psgnunilem3  19408  efgsdm  19642  efgredlemd  19656  efgredlem  19659  efgred  19660  efgrelexlema  19661  efgrelexlemb  19662  prdsgsum  19893  pwspjmhmmgpd  20246  pwsexpg  20247  isrnghm  20359  isabv  20726  islmhm  20961  frgpcyg  21510  psgndiflemB  21537  psgndiflemA  21538  dsmmelbas  21676  frlmipval  21716  frlmphl  21718  uvcf1  21729  islindf  21749  islindf4  21775  psrmulfval  21880  evlslem2  22014  evlslem3  22015  evlslem1  22017  mpfrcl  22020  selvval  22050  psdval  22074  psdcoef  22075  psdadd  22078  psdmul  22081  psdmvr  22084  coe1fval  22118  coe1mul2lem2  22182  coe1tm  22187  madetsumid  22376  mvmulval  22458  marepvval0  22481  mulmarep1gsum2  22489  mdetleib2  22503  m1detdiag  22512  mdetralt  22523  mdetunilem7  22533  mdetunilem9  22535  m2detleiblem3  22544  m2detleiblem4  22545  m2detleib  22546  symgmatr01lem  22568  gsummatr01lem1  22570  gsummatr01lem4  22573  gsummatr01  22574  smadiadetlem3  22583  pmatcoe1fsupp  22616  pmatcollpw3lem  22698  pmatcollpw3fi1lem2  22702  iscnp  23152  1stcfb  23360  ptpjpre1  23486  elpt  23487  elptr  23488  ptpjopn  23527  dfac14  23533  upxp  23538  pthaus  23553  ptrescn  23554  xkoptsub  23569  cnmptkp  23595  xkofvcn  23599  cnmptk1p  23600  cnmptk2  23601  ptunhmeo  23723  ptcmplem3  23969  ptcmplem4  23970  symgtgp  24021  prdstmdd  24039  isucn  24192  imasdsf1olem  24288  prdsxmslem2  24444  tngngp3  24571  nmoval  24630  elcncf  24809  ishtpy  24898  pcoval  24938  om1elbas  24959  elpi1i  24973  iscau  25203  rrxds  25320  rrxdsfival  25340  ehl1eudisval  25348  ehl2eudisval  25350  mbfi1fseqlem6  25648  mbfi1flimlem  25650  isibl  25693  deg1ldg  26024  deg1leb  26027  elply2  26128  elplyr  26133  ne0p  26139  coeeu  26157  coelem  26158  coeeq  26159  coeidlem  26169  elqaalem3  26256  qaa  26258  iaa  26260  aareccl  26261  aannenlem2  26264  aaliou2  26275  dchrptlem2  27203  dchrpt  27205  dchrsum2  27206  sumdchr2  27208  dchrvmaeq0  27442  rpvmasum2  27450  dchrisum0re  27451  ostth  27577  sltval  27586  nolesgn2o  27610  nogesgn1o  27612  noresle  27636  nosupprefixmo  27639  noinfprefixmo  27640  nosupcbv  27641  nosupfv  27645  noinfcbv  27656  noinffv  27660  iscgrg  28490  isismt  28512  israg  28675  iseqlg  28845  brbtwn  28877  brbtwn2  28883  colinearalg  28888  axsegconlem1  28895  axsegcon  28905  ax5seglem5  28911  axpasch  28919  axlowdim  28939  axeuclidlem  28940  axcontlem1  28942  axcontlem2  28943  axcontlem5  28946  vtxdgfval  29446  1egrvtxdg1  29488  isewlk  29581  iswlk  29589  uspgr2wlkeq2  29625  iswlkon  29634  isclwlk  29751  iscrct  29768  iscycl  29769  iswwlks  29814  wwlknon  29835  wlkiswwlks2  29853  wwlksnredwwlkn0  29874  wlksnwwlknvbij  29886  wwlksnextproplem3  29889  wwlksnextprop  29890  umgr2wlk  29927  midwwlks2s3  29930  elwwlks2  29947  elwspths2spth  29948  rusgrnumwwlkslem  29950  rusgrnumwwlkb0  29952  rusgrnumwwlks  29955  isclwwlk  29964  clwlkclwwlklem1  29979  clwwlkn1loopb  30023  clwwlkel  30026  clwwlkf  30027  clwwlkf1  30029  isclwwlknon  30071  clwwlknon1  30077  s2elclwwlknon2  30084  clwwlkvbij  30093  uhgr3cyclex  30162  fusgreg2wsplem  30313  fusgr2wsp2nb  30314  fusgreghash2wsp  30318  2clwwlkel  30329  extwwlkfabel  30333  numclwwlk1lem2fv  30336  numclwwlk1lem2  30340  clwwlknonclwlknonf1o  30342  dlwwlknondlwlknonf1o  30345  numclwwlk2lem1  30356  numclwlk2lem2f  30357  numclwlk2lem2f1o  30359  ex-fv  30423  isnvlem  30590  islno  30733  nmooval  30743  nmblolbi  30780  isphg  30797  ajmoi  30838  ajval  30841  ubthlem3  30852  htthlem  30897  hcau  31164  hlimi  31168  hosmval  31715  hommval  31716  hodmval  31717  hfsmval  31718  hfmmval  31719  adjmo  31812  nmopval  31836  elcnop  31837  ellnop  31838  elunop  31852  elhmop  31853  nmfnval  31856  elcnfn  31862  ellnfn  31863  adjeu  31869  adjval  31870  eigvecval  31876  eigvalfval  31877  adj1  31913  adjeq  31915  hmopadj2  31921  lnopeq0i  31987  lnopeq  31989  elunop2  31993  lnophm  31999  hmopco  32003  nmbdoplb  32005  nmcoplb  32010  lnopcon  32015  lnfn0  32027  lnfnmul  32028  nmbdfnlb  32030  nmcfnlb  32034  lnfncon  32036  riesz4  32044  riesz1  32045  cnlnadjlem9  32055  cnlnadjeu  32058  cnlnssadj  32060  nmopcoi  32075  bra11  32088  cnvbraval  32090  pjss2coi  32144  pjssdif2i  32154  pjssdif1i  32155  pjclem4  32179  pj3si  32187  pj3cor1i  32189  isst  32193  ishst  32194  stri  32237  hstri  32245  aciunf1lem  32644  ismnt  32964  mgcval  32968  fzo0pmtrlast  33061  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem3  33211  elrgspnlem4  33212  elrgspn  33213  elrgspnsubrunlem1  33214  linds2eq  33346  elrspunidl  33393  elrspunsn  33394  dfufd2lem  33514  mplvrpmga  33575  splysubrg  33583  issply  33584  lbsdiflsp0  33639  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  fldextrspunlsplem  33686  fldextrspunlsp  33687  fldext2chn  33741  constrextdg2lem  33761  constrextdg2  33762  lmatval  33826  mdetpmtr1  33836  zarcmplem  33894  ismeas  34212  isrnmeas  34213  cntnevol  34241  carsgval  34316  sitgval  34345  eulerpartleme  34376  eulerpartlemd  34379  eulerpartlemr  34387  eulerpartlemgvv  34389  eulerpart  34395  cndprobval  34446  signstfvneq0  34585  reprsum  34626  reprsuc  34628  reprpmtf1o  34639  reprdifc  34640  breprexp  34646  vtsval  34650  hgt750lemb  34669  hgt750lema  34670  hgt750leme  34671  bnj66  34872  bnj106  34880  bnj125  34884  bnj154  34890  bnj155  34891  bnj526  34900  bnj540  34904  bnj609  34929  bnj611  34930  bnj893  34940  bnj1000  34953  bnj1014  34973  bnj1015  34974  bnj1234  35025  bnj1463  35067  fineqvnttrclse  35144  gblacfnacd  35146  loop1cycl  35181  derangenlem  35215  subfacp1lem3  35226  subfacp1lem5  35228  subfacp1lem6  35229  subfacp1  35230  sconnpht  35273  cnpconn  35274  txpconn  35276  ptpconn  35277  indispconn  35278  connpconn  35279  cvxpconn  35286  cvmliftmo  35328  cvmliftlem14  35341  cvmliftlem15  35342  cvmliftiota  35345  cvmlift2  35360  cvmliftphtlem  35361  cvmlift3lem2  35364  cvmlift3lem6  35368  cvmlift3lem7  35369  cvmlift3lem9  35371  cvmlift3  35372  satfv1lem  35406  satfv1  35407  sategoelfvb  35463  mrsubff1  35558  mrsub0  35560  mrsubccat  35562  mrsubcn  35563  elmsubrn  35572  msubrn  35573  msubco  35575  msubvrs  35604  mclsax  35613  shftvalg  35776  fwddifval  36204  fwddifnval  36205  bj-evalval  37117  unceq  37645  matunitlindflem2  37665  poimirlem17  37685  poimirlem20  37688  poimirlem22  37690  poimirlem23  37691  poimirlem27  37695  poimirlem28  37696  poimirlem30  37698  poimirlem31  37699  poimirlem32  37700  poimir  37701  broucube  37702  voliunnfl  37712  volsupnfl  37713  itg2addnclem  37719  itg2addnclem3  37721  itg2addnc  37722  ftc1anclem2  37742  ftc1anclem5  37745  upixp  37777  fdc  37793  isismty  37849  rrnmval  37876  elghomlem2OLD  37934  isrngohom  38013  islfl  39107  isopos  39227  islaut  40130  ispautN  40146  isldil  40157  isltrn  40166  ltrnid  40182  ltrneq2  40195  isdilN  40201  istrnN  40204  trlval  40209  ltrneq3  40255  cdleme50ex  40606  cdleme  40607  cdlemg1a  40617  ltrniotaval  40628  ltrniotavalbN  40631  cdlemeiota  40632  cdlemg2jlemOLDN  40640  cdlemg2fvlem  40641  cdlemg2klem  40642  istendo  40807  tendoplcbv  40822  tendopl  40823  tendoicbv  40840  tendoi  40841  tendoid0  40872  tendo1ne0  40875  cdlemksv2  40894  cdlemkuv2  40914  cdlemk33N  40956  cdlemk34  40957  cdlemk36  40960  cdlemk19u  41017  cdlemk  41021  tendoex  41022  dvavsca  41064  dvhvscacbv  41145  dvhvscaval  41146  dicopelval  41224  dicelval1sta  41234  diclspsn  41241  dihmeetlem13N  41366  dih1dimatlem0  41375  dih1dimatlem  41376  dihpN  41383  islpolN  41530  hdmap1fval  41843  hdmapfval  41874  sticksstones1  42187  sticksstones2  42188  sticksstones3  42189  sticksstones8  42194  sticksstones10  42196  sticksstones11  42197  sticksstones12a  42198  sticksstones12  42199  sticksstones15  42202  frlmsnic  42581  uvcn0  42583  pwsgprod  42585  mplmapghm  42597  evlsvval  42601  evlsvvval  42604  evlsvarval  42606  evlsbagval  42607  selvvvval  42626  evlselv  42628  fsuppssindlem2  42633  fsuppssind  42634  prjspnfv01  42665  prjspner01  42666  prjspner1  42667  sn-isghm  42714  ismrc  42742  mzpclval  42766  mzpsubst  42789  mzprename  42790  mzpcompact2lem  42792  eldioph  42799  eldioph2  42803  eldioph2b  42804  eldioph3  42807  rexrabdioph  42835  2rexfrabdioph  42837  3rexfrabdioph  42838  4rexfrabdioph  42839  6rexfrabdioph  42840  7rexfrabdioph  42841  eldioph4i  42853  rabren3dioph  42856  mzpcong  43013  jm2.27dlem1  43050  wepwsolem  43083  aomclem6  43100  aomclem8  43102  dfac11  43103  dgraalem  43186  dgraaub  43189  dgraa0p  43190  mpaaeu  43191  mpaalem  43193  aaitgo  43203  rngunsnply  43210  cantnfresb  43365  tfsconcatun  43378  nvocnvb  43463  eliunov2  43720  rfovcnvfvd  44048  fsovfvd  44051  fsovcnvlem  44054  dssmapfv2d  44059  dssmapnvod  44061  clsk1independent  44087  ntrclskb  44110  ntrclsk13  44112  gneispace2  44173  mnringmulrvald  44268  dvconstbi  44375  addrval  44506  subrval  44507  mulvval  44508  relpeq1  44985  fnchoice  45074  refsum2cnlem1  45082  choicefi  45245  axccdom  45267  fmulcl  45629  fmuldfeqlem1  45630  mccllem  45645  mccl  45646  climf  45670  climf2  45712  dvnprodlem1  45992  dvnprodlem3  45994  dvnprod  45995  stoweidlem2  46048  stoweidlem6  46052  stoweidlem8  46054  stoweidlem9  46055  stoweidlem15  46061  stoweidlem16  46062  stoweidlem17  46063  stoweidlem18  46064  stoweidlem21  46067  stoweidlem27  46073  stoweidlem31  46077  stoweidlem36  46082  stoweidlem37  46083  stoweidlem41  46087  stoweidlem43  46089  stoweidlem44  46090  stoweidlem45  46091  stoweidlem46  46092  stoweidlem48  46094  stoweidlem51  46097  stoweidlem55  46101  stoweidlem59  46105  stoweidlem60  46106  stoweidlem62  46108  fourierdlem2  46155  fourierdlem3  46156  elaa2lem  46279  etransclem11  46291  etransclem24  46304  etransclem26  46306  etransclem28  46308  etransclem35  46315  rrndistlt  46336  ioorrnopn  46351  subsaliuncllem  46403  sge0val  46412  ismea  46497  caragenval  46539  isome  46540  isomenndlem  46576  hoicvrrex  46602  ovnlecvr  46604  ovncvrrp  46610  ovn0lem  46611  ovnsubaddlem1  46616  ovnsubadd  46618  hsphoif  46622  hoidmvval  46623  hsphoival  46625  hoidmvlelem3  46643  hoidmvlelem5  46645  hoidmvle  46646  ovnhoilem1  46647  ovnhoi  46649  ovnlecvr2  46656  ovncvr2  46657  hoidifhspval2  46661  hoiqssbllem2  46669  hspmbllem2  46673  hspmbllem3  46674  hspmbl  46675  ovnovollem1  46702  smfmullem2  46838  smfmul  46841  smfpimcclem  46853  sinnpoly  46930  cfsetsnfsetfv  47096  cfsetsnfsetfo  47099  iccpart  47455  iccpartiun  47473  icceuelpart  47475  nnsum3primes4  47827  nnsum3primesgbe  47831  nnsum4primesodd  47835  nnsum4primesoddALTV  47836  nnsum4primeseven  47839  nnsum4primesevenALTV  47840  bgoldbtbnd  47848  isisubgr  47901  isgrim  47921  grimidvtxedg  47924  grimcnv  47927  grimco  47928  isuspgrim0  47933  gricushgr  47956  ushggricedg  47966  uhgrimisgrgric  47970  isgrtri  47982  isubgr3stgrlem3  48007  isubgr3stgr  48014  isgrlim  48021  uspgrlim  48031  grlicref  48051  grlicsym  48052  grlictr  48054  grlimedgnedg  48170  isupwlk  48175  lincval  48449  lincdifsn  48464  linindslinci  48488  lindslinindsimp1  48497  linds0  48505  el0ldep  48506  lindsrng01  48508  snlindsntorlem  48510  ldepspr  48513  islindeps2  48523  zlmodzxzldep  48544  bigoval  48589  elbigo  48591  0aryfvalelfv  48675  1arympt1fv  48679  1arymaptfv  48680  1arymaptfo  48683  2arymptfv  48690  2arymaptfv  48691  2arymaptfo  48694  prelrrx2b  48754  rrx2plord  48760  rrx2vlinest  48781  rrx2linesl  48783  elrrx2linest2  48785  line2ylem  48791  line2xlem  48793  itsclc0  48811  itsclc0b  48812  itscnhlinecirc02p  48825  elfvne0  48888  iinfprg  49099  thincciso  49493  thinccisod  49494  setrecseq  49725  aacllem  49841