Theorem fveq1 6874

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 5121	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6514	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6538	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6538	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2795	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5119  ℩cio 6481  ‘cfv 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538

This theorem is referenced by:  fveq1i  6876  fveq1d  6877  iffv  6892  fvmptd3f  7000  fvmptdv2  7003  eqfnun  7026  fsnex  7275  f1prex  7276  isoeq1  7309  oveq  7409  elovmpt3imp  7662  ofrfvalg  7677  offval  7678  offval3  7979  bropopvvv  8087  bropfvvvvlem  8088  poseq  8155  soseq  8156  frrlem1  8283  frrlem13  8295  wfrlem1OLD  8320  wfrlem3OLDa  8323  wfrlem15OLD  8335  smoeq  8362  tfrlem12  8401  tz7.44-2  8419  tz7.44-3  8420  rdgeq1  8423  fsetfocdm  8873  fsetprcnex  8874  mapsncnv  8905  elixp2  8913  resixpfo  8948  elixpsn  8949  mapsnend  9048  enfixsn  9093  mapxpen  9155  ac6sfi  9290  ordtypelem7  9536  wemaplem1  9558  ixpiunwdom  9602  oemapval  9695  cantnf  9705  wemapwe  9709  cnfcom3clem  9717  ssttrcl  9727  ttrcltr  9728  ttrclss  9732  ttrclselem2  9738  updjud  9946  infxpenc2lem2  10032  fseqenlem1  10036  dfac8clem  10044  ac5num  10048  acni  10057  acni2  10058  acnlem  10060  dfac4  10134  dfac5lem5  10139  dfac2a  10142  dfac9  10149  dfacacn  10154  dfac12lem1  10156  dfac12r  10159  cofsmo  10281  cfsmolem  10282  cfsmo  10283  cfcoflem  10284  coftr  10285  alephsing  10288  isfin3ds  10341  fin23lem17  10350  fin23lem32  10356  fin23lem39  10362  isf33lem  10378  isf34lem6  10392  axcc2lem  10448  axcc3  10450  axdc2lem  10460  axdc3lem2  10463  axdc3lem3  10464  axdc3  10466  axdc4lem  10467  axcclem  10469  ac6num  10491  axdclem2  10532  konigthlem  10580  inar1  10787  1fv  13662  axdc4uzlem  13999  seqeq3  14022  seqof  14075  ccatfval  14589  wrdl1s1  14630  ccat1st1st  14644  cshf1  14826  cshweqrep  14837  wrdlen2i  14959  wwlktovf  14973  wwlktovf1  14974  wwlktovfo  14975  wrd2f1tovbij  14977  rtrclreclem1  15074  dfrtrclrec2  15075  rtrclreclem2  15076  rtrclreclem4  15078  dfrtrcl2  15079  clim  15508  rlim  15509  ello1  15529  elo1  15540  summo  15731  fsum  15734  prodmo  15950  fprod  15955  bpolylem  16062  bpolyval  16063  vdwlem6  17004  vdwlem8  17006  ramcl  17047  strfvnd  17202  prdsplusgval  17485  prdsmulrval  17487  prdsleval  17489  prdsdsval  17490  prdsvscaval  17491  xpsff1o  17579  isacs2  17663  isnat  17961  yonedalem3b  18289  yonedainv  18291  ismgmhm  18672  ismhm  18761  prdspjmhm  18805  isgrpinv  18974  pwsmulg  19100  isghm  19196  isghmOLD  19197  cayleylem2  19392  symgfix2  19395  gsmsymgrfix  19407  gsmsymgreq  19411  symgfixelq  19412  pmtr3ncomlem2  19453  pmtrdifel  19459  pmtrdifwrdel  19464  pmtrdifwrdel2  19465  psgnunilem2  19474  psgnunilem3  19475  efgsdm  19709  efgredlemd  19723  efgredlem  19726  efgred  19727  efgrelexlema  19728  efgrelexlemb  19729  prdsgsum  19960  pwspjmhmmgpd  20286  pwsexpg  20287  isrnghm  20399  isabv  20769  islmhm  20983  frgpcyg  21532  psgndiflemB  21558  psgndiflemA  21559  dsmmelbas  21697  frlmipval  21737  frlmphl  21739  uvcf1  21750  islindf  21770  islindf4  21796  psrmulfval  21901  evlslem2  22035  evlslem3  22036  evlslem1  22038  mpfrcl  22041  selvval  22071  psdval  22095  psdcoef  22096  psdadd  22099  psdmul  22102  psdmvr  22105  coe1fval  22139  coe1mul2lem2  22203  coe1tm  22208  madetsumid  22397  mvmulval  22479  marepvval0  22502  mulmarep1gsum2  22510  mdetleib2  22524  m1detdiag  22533  mdetralt  22544  mdetunilem7  22554  mdetunilem9  22556  m2detleiblem3  22565  m2detleiblem4  22566  m2detleib  22567  symgmatr01lem  22589  gsummatr01lem1  22591  gsummatr01lem4  22594  gsummatr01  22595  smadiadetlem3  22604  pmatcoe1fsupp  22637  pmatcollpw3lem  22719  pmatcollpw3fi1lem2  22723  iscnp  23173  1stcfb  23381  ptpjpre1  23507  elpt  23508  elptr  23509  ptpjopn  23548  dfac14  23554  upxp  23559  pthaus  23574  ptrescn  23575  xkoptsub  23590  cnmptkp  23616  xkofvcn  23620  cnmptk1p  23621  cnmptk2  23622  ptunhmeo  23744  ptcmplem3  23990  ptcmplem4  23991  symgtgp  24042  prdstmdd  24060  isucn  24214  imasdsf1olem  24310  prdsxmslem2  24466  tngngp3  24593  nmoval  24652  elcncf  24831  ishtpy  24920  pcoval  24960  om1elbas  24981  elpi1i  24995  iscau  25226  rrxds  25343  rrxdsfival  25363  ehl1eudisval  25371  ehl2eudisval  25373  mbfi1fseqlem6  25671  mbfi1flimlem  25673  isibl  25716  deg1ldg  26047  deg1leb  26050  elply2  26151  elplyr  26156  ne0p  26162  coeeu  26180  coelem  26181  coeeq  26182  coeidlem  26192  elqaalem3  26279  qaa  26281  iaa  26283  aareccl  26284  aannenlem2  26287  aaliou2  26298  dchrptlem2  27226  dchrpt  27228  dchrsum2  27229  sumdchr2  27231  dchrvmaeq0  27465  rpvmasum2  27473  dchrisum0re  27474  ostth  27600  sltval  27609  nolesgn2o  27633  nogesgn1o  27635  noresle  27659  nosupprefixmo  27662  noinfprefixmo  27663  nosupcbv  27664  nosupfv  27668  noinfcbv  27679  noinffv  27683  iscgrg  28437  isismt  28459  israg  28622  iseqlg  28792  brbtwn  28824  brbtwn2  28830  colinearalg  28835  axsegconlem1  28842  axsegcon  28852  ax5seglem5  28858  axpasch  28866  axlowdim  28886  axeuclidlem  28887  axcontlem1  28889  axcontlem2  28890  axcontlem5  28893  vtxdgfval  29393  1egrvtxdg1  29435  isewlk  29528  iswlk  29536  uspgr2wlkeq2  29573  iswlkon  29583  isclwlk  29701  iscrct  29718  iscycl  29719  iswwlks  29764  wwlknon  29785  wlkiswwlks2  29803  wwlksnredwwlkn0  29824  wlksnwwlknvbij  29836  wwlksnextproplem3  29839  wwlksnextprop  29840  umgr2wlk  29877  midwwlks2s3  29880  elwwlks2  29894  elwspths2spth  29895  rusgrnumwwlkslem  29897  rusgrnumwwlkb0  29899  rusgrnumwwlks  29902  isclwwlk  29911  clwlkclwwlklem1  29926  clwwlkn1loopb  29970  clwwlkel  29973  clwwlkf  29974  clwwlkf1  29976  isclwwlknon  30018  clwwlknon1  30024  s2elclwwlknon2  30031  clwwlkvbij  30040  uhgr3cyclex  30109  fusgreg2wsplem  30260  fusgr2wsp2nb  30261  fusgreghash2wsp  30265  2clwwlkel  30276  extwwlkfabel  30280  numclwwlk1lem2fv  30283  numclwwlk1lem2  30287  clwwlknonclwlknonf1o  30289  dlwwlknondlwlknonf1o  30292  numclwwlk2lem1  30303  numclwlk2lem2f  30304  numclwlk2lem2f1o  30306  ex-fv  30370  isnvlem  30537  islno  30680  nmooval  30690  nmblolbi  30727  isphg  30744  ajmoi  30785  ajval  30788  ubthlem3  30799  htthlem  30844  hcau  31111  hlimi  31115  hosmval  31662  hommval  31663  hodmval  31664  hfsmval  31665  hfmmval  31666  adjmo  31759  nmopval  31783  elcnop  31784  ellnop  31785  elunop  31799  elhmop  31800  nmfnval  31803  elcnfn  31809  ellnfn  31810  adjeu  31816  adjval  31817  eigvecval  31823  eigvalfval  31824  adj1  31860  adjeq  31862  hmopadj2  31868  lnopeq0i  31934  lnopeq  31936  elunop2  31940  lnophm  31946  hmopco  31950  nmbdoplb  31952  nmcoplb  31957  lnopcon  31962  lnfn0  31974  lnfnmul  31975  nmbdfnlb  31977  nmcfnlb  31981  lnfncon  31983  riesz4  31991  riesz1  31992  cnlnadjlem9  32002  cnlnadjeu  32005  cnlnssadj  32007  nmopcoi  32022  bra11  32035  cnvbraval  32037  pjss2coi  32091  pjssdif2i  32101  pjssdif1i  32102  pjclem4  32126  pj3si  32134  pj3cor1i  32136  isst  32140  ishst  32141  stri  32184  hstri  32192  aciunf1lem  32586  ismnt  32909  mgcval  32913  ischn  32932  chnind  32937  chnub  32938  fzo0pmtrlast  33049  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem3  33185  elrgspnlem4  33186  elrgspn  33187  elrgspnsubrunlem1  33188  linds2eq  33342  elrspunidl  33389  elrspunsn  33390  dfufd2lem  33510  lbsdiflsp0  33612  fedgmullem1  33615  fedgmullem2  33616  fedgmul  33617  fldextrspunlsplem  33660  fldextrspunlsp  33661  fldext2chn  33708  constrextdg2lem  33728  constrextdg2  33729  lmatval  33790  mdetpmtr1  33800  zarcmplem  33858  ismeas  34176  isrnmeas  34177  cntnevol  34205  carsgval  34281  sitgval  34310  eulerpartleme  34341  eulerpartlemd  34344  eulerpartlemr  34352  eulerpartlemgvv  34354  eulerpart  34360  cndprobval  34411  signstfvneq0  34550  reprsum  34591  reprsuc  34593  reprpmtf1o  34604  reprdifc  34605  breprexp  34611  vtsval  34615  hgt750lemb  34634  hgt750lema  34635  hgt750leme  34636  bnj66  34837  bnj106  34845  bnj125  34849  bnj154  34855  bnj155  34856  bnj526  34865  bnj540  34869  bnj609  34894  bnj611  34895  bnj893  34905  bnj1000  34918  bnj1014  34938  bnj1015  34939  bnj1234  34990  bnj1463  35032  gblacfnacd  35076  loop1cycl  35105  derangenlem  35139  subfacp1lem3  35150  subfacp1lem5  35152  subfacp1lem6  35153  subfacp1  35154  sconnpht  35197  cnpconn  35198  txpconn  35200  ptpconn  35201  indispconn  35202  connpconn  35203  cvxpconn  35210  cvmliftmo  35252  cvmliftlem14  35265  cvmliftlem15  35266  cvmliftiota  35269  cvmlift2  35284  cvmliftphtlem  35285  cvmlift3lem2  35288  cvmlift3lem6  35292  cvmlift3lem7  35293  cvmlift3lem9  35295  cvmlift3  35296  satfv1lem  35330  satfv1  35331  sategoelfvb  35387  mrsubff1  35482  mrsub0  35484  mrsubccat  35486  mrsubcn  35487  elmsubrn  35496  msubrn  35497  msubco  35499  msubvrs  35528  mclsax  35537  shftvalg  35695  fwddifval  36126  fwddifnval  36127  bj-evalval  37039  unceq  37567  matunitlindflem2  37587  poimirlem17  37607  poimirlem20  37610  poimirlem22  37612  poimirlem23  37613  poimirlem27  37617  poimirlem28  37618  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  poimir  37623  broucube  37624  voliunnfl  37634  volsupnfl  37635  itg2addnclem  37641  itg2addnclem3  37643  itg2addnc  37644  ftc1anclem2  37664  ftc1anclem5  37667  upixp  37699  fdc  37715  isismty  37771  rrnmval  37798  elghomlem2OLD  37856  isrngohom  37935  islfl  39024  isopos  39144  islaut  40048  ispautN  40064  isldil  40075  isltrn  40084  ltrnid  40100  ltrneq2  40113  isdilN  40119  istrnN  40122  trlval  40127  ltrneq3  40173  cdleme50ex  40524  cdleme  40525  cdlemg1a  40535  ltrniotaval  40546  ltrniotavalbN  40549  cdlemeiota  40550  cdlemg2jlemOLDN  40558  cdlemg2fvlem  40559  cdlemg2klem  40560  istendo  40725  tendoplcbv  40740  tendopl  40741  tendoicbv  40758  tendoi  40759  tendoid0  40790  tendo1ne0  40793  cdlemksv2  40812  cdlemkuv2  40832  cdlemk33N  40874  cdlemk34  40875  cdlemk36  40878  cdlemk19u  40935  cdlemk  40939  tendoex  40940  dvavsca  40982  dvhvscacbv  41063  dvhvscaval  41064  dicopelval  41142  dicelval1sta  41152  diclspsn  41159  dihmeetlem13N  41284  dih1dimatlem0  41293  dih1dimatlem  41294  dihpN  41301  islpolN  41448  hdmap1fval  41761  hdmapfval  41792  sticksstones1  42105  sticksstones2  42106  sticksstones3  42107  sticksstones8  42112  sticksstones10  42114  sticksstones11  42115  sticksstones12a  42116  sticksstones12  42117  sticksstones15  42120  frlmsnic  42510  uvcn0  42512  pwsgprod  42514  mplmapghm  42526  evlsvval  42530  evlsvvval  42533  evlsvarval  42535  evlsbagval  42536  selvvvval  42555  evlselv  42557  fsuppssindlem2  42562  fsuppssind  42563  prjspnfv01  42594  prjspner01  42595  prjspner1  42596  sn-isghm  42643  ismrc  42671  mzpclval  42695  mzpsubst  42718  mzprename  42719  mzpcompact2lem  42721  eldioph  42728  eldioph2  42732  eldioph2b  42733  eldioph3  42736  rexrabdioph  42764  2rexfrabdioph  42766  3rexfrabdioph  42767  4rexfrabdioph  42768  6rexfrabdioph  42769  7rexfrabdioph  42770  eldioph4i  42782  rabren3dioph  42785  mzpcong  42943  jm2.27dlem1  42980  wepwsolem  43013  aomclem6  43030  aomclem8  43032  dfac11  43033  dgraalem  43116  dgraaub  43119  dgraa0p  43120  mpaaeu  43121  mpaalem  43123  aaitgo  43133  rngunsnply  43140  cantnfresb  43295  tfsconcatun  43308  nvocnvb  43393  eliunov2  43650  rfovcnvfvd  43978  fsovfvd  43981  fsovcnvlem  43984  dssmapfv2d  43989  dssmapnvod  43991  clsk1independent  44017  ntrclskb  44040  ntrclsk13  44042  gneispace2  44103  mnringmulrvald  44199  dvconstbi  44306  addrval  44438  subrval  44439  mulvval  44440  relpeq1  44917  fnchoice  45001  refsum2cnlem1  45009  choicefi  45172  axccdom  45194  fmulcl  45558  fmuldfeqlem1  45559  mccllem  45574  mccl  45575  climf  45599  climf2  45643  dvnprodlem1  45923  dvnprodlem3  45925  dvnprod  45926  stoweidlem2  45979  stoweidlem6  45983  stoweidlem8  45985  stoweidlem9  45986  stoweidlem15  45992  stoweidlem16  45993  stoweidlem17  45994  stoweidlem18  45995  stoweidlem21  45998  stoweidlem27  46004  stoweidlem31  46008  stoweidlem36  46013  stoweidlem37  46014  stoweidlem41  46018  stoweidlem43  46020  stoweidlem44  46021  stoweidlem45  46022  stoweidlem46  46023  stoweidlem48  46025  stoweidlem51  46028  stoweidlem55  46032  stoweidlem59  46036  stoweidlem60  46037  stoweidlem62  46039  fourierdlem2  46086  fourierdlem3  46087  elaa2lem  46210  etransclem11  46222  etransclem24  46235  etransclem26  46237  etransclem28  46239  etransclem35  46246  rrndistlt  46267  ioorrnopn  46282  subsaliuncllem  46334  sge0val  46343  ismea  46428  caragenval  46470  isome  46471  isomenndlem  46507  hoicvrrex  46533  ovnlecvr  46535  ovncvrrp  46541  ovn0lem  46542  ovnsubaddlem1  46547  ovnsubadd  46549  hsphoif  46553  hoidmvval  46554  hsphoival  46556  hoidmvlelem3  46574  hoidmvlelem5  46576  hoidmvle  46577  ovnhoilem1  46578  ovnhoi  46580  ovnlecvr2  46587  ovncvr2  46588  hoidifhspval2  46592  hoiqssbllem2  46600  hspmbllem2  46604  hspmbllem3  46605  hspmbl  46606  ovnovollem1  46633  smfmullem2  46769  smfmul  46772  smfpimcclem  46784  tworepnotupword  46863  cfsetsnfsetfv  47034  cfsetsnfsetfo  47037  iccpart  47378  iccpartiun  47396  icceuelpart  47398  nnsum3primes4  47750  nnsum3primesgbe  47754  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  bgoldbtbnd  47771  isisubgr  47823  isgrim  47843  grimidvtxedg  47846  grimcnv  47849  grimco  47850  isuspgrim0  47855  gricushgr  47878  ushggricedg  47888  uhgrimisgrgric  47892  isgrtri  47903  isubgr3stgrlem3  47928  isubgr3stgr  47935  isgrlim  47942  uspgrlim  47952  grlicref  47965  grlicsym  47966  grlictr  47968  isupwlk  48059  lincval  48333  lincdifsn  48348  linindslinci  48372  lindslinindsimp1  48381  linds0  48389  el0ldep  48390  lindsrng01  48392  snlindsntorlem  48394  ldepspr  48397  islindeps2  48407  zlmodzxzldep  48428  bigoval  48477  elbigo  48479  0aryfvalelfv  48563  1arympt1fv  48567  1arymaptfv  48568  1arymaptfo  48571  2arymptfv  48578  2arymaptfv  48579  2arymaptfo  48582  prelrrx2b  48642  rrx2plord  48648  rrx2vlinest  48669  rrx2linesl  48671  elrrx2linest2  48673  line2ylem  48679  line2xlem  48681  itsclc0  48699  itsclc0b  48700  itscnhlinecirc02p  48713  elfvne0  48775  iinfprg  48974  thincciso  49287  thinccisod  49288  setrecseq  49497  aacllem  49613