Theorem fveq1 6839

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 5087	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6482	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6506	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6506	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5085  ℩cio 6452  ‘cfv 6498

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506

This theorem is referenced by:  fveq1i  6841  fveq1d  6842  iffv  6857  fvmptd3f  6963  fvmptdv2  6966  eqfnun  6989  fsnex  7238  f1prex  7239  isoeq1  7272  oveq  7373  elovmpt3imp  7624  ofrfvalg  7639  offval  7640  offval3  7935  bropopvvv  8040  bropfvvvvlem  8041  poseq  8108  soseq  8109  frrlem1  8236  frrlem13  8248  smoeq  8290  tfrlem12  8328  tz7.44-2  8346  tz7.44-3  8347  rdgeq1  8350  fsetfocdm  8808  fsetprcnex  8809  mapsncnv  8841  elixp2  8849  resixpfo  8884  elixpsn  8885  mapsnend  8983  enfixsn  9024  mapxpen  9081  ac6sfi  9194  ordtypelem7  9439  wemaplem1  9461  ixpiunwdom  9505  oemapval  9604  cantnf  9614  wemapwe  9618  cnfcom3clem  9626  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  updjud  9858  infxpenc2lem2  9942  fseqenlem1  9946  dfac8clem  9954  ac5num  9958  acni  9967  acni2  9968  acnlem  9970  dfac4  10044  dfac5lem5  10049  dfac2a  10052  dfac9  10059  dfacacn  10064  dfac12lem1  10066  dfac12r  10069  cofsmo  10191  cfsmolem  10192  cfsmo  10193  cfcoflem  10194  coftr  10195  alephsing  10198  isfin3ds  10251  fin23lem17  10260  fin23lem32  10266  fin23lem39  10272  isf33lem  10288  isf34lem6  10302  axcc2lem  10358  axcc3  10360  axdc2lem  10370  axdc3lem2  10373  axdc3lem3  10374  axdc3  10376  axdc4lem  10377  axcclem  10379  ac6num  10401  axdclem2  10442  konigthlem  10491  inar1  10698  1fv  13601  axdc4uzlem  13945  seqeq3  13968  seqof  14021  ccatfval  14535  wrdl1s1  14577  ccat1st1st  14591  cshf1  14772  cshweqrep  14783  wrdlen2i  14904  wwlktovf  14918  wwlktovf1  14919  wwlktovfo  14920  wrd2f1tovbij  14922  rtrclreclem1  15019  dfrtrclrec2  15020  rtrclreclem2  15021  rtrclreclem4  15023  dfrtrcl2  15024  clim  15456  rlim  15457  ello1  15477  elo1  15488  summo  15679  fsum  15682  prodmo  15901  fprod  15906  bpolylem  16013  bpolyval  16014  vdwlem6  16957  vdwlem8  16959  ramcl  17000  strfvnd  17155  prdsplusgval  17436  prdsmulrval  17438  prdsleval  17440  prdsdsval  17441  prdsvscaval  17442  xpsff1o  17531  isacs2  17619  isnat  17917  yonedalem3b  18245  yonedainv  18247  ischn  18573  chnind  18587  chnub  18588  ismgmhm  18664  ismhm  18753  prdspjmhm  18797  isgrpinv  18969  pwsmulg  19095  isghm  19190  isghmOLD  19191  cayleylem2  19388  symgfix2  19391  gsmsymgrfix  19403  gsmsymgreq  19407  symgfixelq  19408  pmtr3ncomlem2  19449  pmtrdifel  19455  pmtrdifwrdel  19460  pmtrdifwrdel2  19461  psgnunilem2  19470  psgnunilem3  19471  efgsdm  19705  efgredlemd  19719  efgredlem  19722  efgred  19723  efgrelexlema  19724  efgrelexlemb  19725  prdsgsum  19956  pwspjmhmmgpd  20307  pwsexpg  20308  pwsgprod  20309  isrnghm  20421  isabv  20788  islmhm  21022  frgpcyg  21553  psgndiflemB  21580  psgndiflemA  21581  dsmmelbas  21719  frlmipval  21759  frlmphl  21761  uvcf1  21772  islindf  21792  islindf4  21818  psrmulfval  21922  evlslem2  22057  evlslem3  22058  evlslem1  22060  mpfrcl  22063  evlsvval  22068  evlsvvval  22071  selvval  22101  psdval  22125  psdcoef  22126  psdadd  22129  psdmul  22132  psdmvr  22135  coe1fval  22169  coe1mul2lem2  22233  coe1tm  22238  madetsumid  22426  mvmulval  22508  marepvval0  22531  mulmarep1gsum2  22539  mdetleib2  22553  m1detdiag  22562  mdetralt  22573  mdetunilem7  22583  mdetunilem9  22585  m2detleiblem3  22594  m2detleiblem4  22595  m2detleib  22596  symgmatr01lem  22618  gsummatr01lem1  22620  gsummatr01lem4  22623  gsummatr01  22624  smadiadetlem3  22633  pmatcoe1fsupp  22666  pmatcollpw3lem  22748  pmatcollpw3fi1lem2  22752  iscnp  23202  1stcfb  23410  ptpjpre1  23536  elpt  23537  elptr  23538  ptpjopn  23577  dfac14  23583  upxp  23588  pthaus  23603  ptrescn  23604  xkoptsub  23619  cnmptkp  23645  xkofvcn  23649  cnmptk1p  23650  cnmptk2  23651  ptunhmeo  23773  ptcmplem3  24019  ptcmplem4  24020  symgtgp  24071  prdstmdd  24089  isucn  24242  imasdsf1olem  24338  prdsxmslem2  24494  tngngp3  24621  nmoval  24680  elcncf  24856  ishtpy  24939  pcoval  24978  om1elbas  24999  elpi1i  25013  iscau  25243  rrxds  25360  rrxdsfival  25380  ehl1eudisval  25388  ehl2eudisval  25390  mbfi1fseqlem6  25687  mbfi1flimlem  25689  isibl  25732  deg1ldg  26057  deg1leb  26060  elply2  26161  elplyr  26166  ne0p  26172  coeeu  26190  coelem  26191  coeeq  26192  coeidlem  26202  elqaalem3  26287  qaa  26289  iaa  26291  aareccl  26292  aannenlem2  26295  aaliou2  26306  dchrptlem2  27228  dchrpt  27230  dchrsum2  27231  sumdchr2  27233  dchrvmaeq0  27467  rpvmasum2  27475  dchrisum0re  27476  ostth  27602  ltsval  27611  nolesgn2o  27635  nogesgn1o  27637  noresle  27661  nosupprefixmo  27664  noinfprefixmo  27665  nosupcbv  27666  nosupfv  27670  noinfcbv  27681  noinffv  27685  iscgrg  28580  isismt  28602  israg  28765  iseqlg  28935  brbtwn  28968  brbtwn2  28974  colinearalg  28979  axsegconlem1  28986  axsegcon  28996  ax5seglem5  29002  axpasch  29010  axlowdim  29030  axeuclidlem  29031  axcontlem1  29033  axcontlem2  29034  axcontlem5  29037  vtxdgfval  29536  1egrvtxdg1  29578  isewlk  29671  iswlk  29679  uspgr2wlkeq2  29715  iswlkon  29724  isclwlk  29841  iscrct  29858  iscycl  29859  iswwlks  29904  wwlknon  29925  wlkiswwlks2  29943  wwlksnredwwlkn0  29964  wlksnwwlknvbij  29976  wwlksnextproplem3  29979  wwlksnextprop  29980  umgr2wlk  30017  midwwlks2s3  30020  elwwlks2  30037  elwspths2spth  30038  rusgrnumwwlkslem  30040  rusgrnumwwlkb0  30042  rusgrnumwwlks  30045  isclwwlk  30054  clwlkclwwlklem1  30069  clwwlkn1loopb  30113  clwwlkel  30116  clwwlkf  30117  clwwlkf1  30119  isclwwlknon  30161  clwwlknon1  30167  s2elclwwlknon2  30174  clwwlkvbij  30183  uhgr3cyclex  30252  fusgreg2wsplem  30403  fusgr2wsp2nb  30404  fusgreghash2wsp  30408  2clwwlkel  30419  extwwlkfabel  30423  numclwwlk1lem2fv  30426  numclwwlk1lem2  30430  clwwlknonclwlknonf1o  30432  dlwwlknondlwlknonf1o  30435  numclwwlk2lem1  30446  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  ex-fv  30513  isnvlem  30681  islno  30824  nmooval  30834  nmblolbi  30871  isphg  30888  ajmoi  30929  ajval  30932  ubthlem3  30943  htthlem  30988  hcau  31255  hlimi  31259  hosmval  31806  hommval  31807  hodmval  31808  hfsmval  31809  hfmmval  31810  adjmo  31903  nmopval  31927  elcnop  31928  ellnop  31929  elunop  31943  elhmop  31944  nmfnval  31947  elcnfn  31953  ellnfn  31954  adjeu  31960  adjval  31961  eigvecval  31967  eigvalfval  31968  adj1  32004  adjeq  32006  hmopadj2  32012  lnopeq0i  32078  lnopeq  32080  elunop2  32084  lnophm  32090  hmopco  32094  nmbdoplb  32096  nmcoplb  32101  lnopcon  32106  lnfn0  32118  lnfnmul  32119  nmbdfnlb  32121  nmcfnlb  32125  lnfncon  32127  riesz4  32135  riesz1  32136  cnlnadjlem9  32146  cnlnadjeu  32149  cnlnssadj  32151  nmopcoi  32166  bra11  32179  cnvbraval  32181  pjss2coi  32235  pjssdif2i  32245  pjssdif1i  32246  pjclem4  32270  pj3si  32278  pj3cor1i  32280  isst  32284  ishst  32285  stri  32328  hstri  32336  aciunf1lem  32735  ismnt  33043  mgcval  33047  fzo0pmtrlast  33153  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspn  33307  elrgspnsubrunlem1  33308  linds2eq  33441  elrspunidl  33488  elrspunsn  33489  dfufd2lem  33609  extvfv  33677  extvfvv  33678  extvfvcl  33680  evlvarval  33685  evlextv  33686  mplvrpmga  33689  splysubrg  33704  issply  33705  vietalem  33723  vieta  33724  lbsdiflsp0  33770  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  fldextrspunlsplem  33817  fldextrspunlsp  33818  fldext2chn  33872  constrextdg2lem  33892  constrextdg2  33893  lmatval  33957  mdetpmtr1  33967  zarcmplem  34025  ismeas  34343  isrnmeas  34344  cntnevol  34372  carsgval  34447  sitgval  34476  eulerpartleme  34507  eulerpartlemd  34510  eulerpartlemr  34518  eulerpartlemgvv  34520  eulerpart  34526  cndprobval  34577  signstfvneq0  34716  reprsum  34757  reprsuc  34759  reprpmtf1o  34770  reprdifc  34771  breprexp  34777  vtsval  34781  hgt750lemb  34800  hgt750lema  34801  hgt750leme  34802  bnj66  35002  bnj106  35010  bnj125  35014  bnj154  35020  bnj155  35021  bnj526  35030  bnj540  35034  bnj609  35059  bnj611  35060  bnj893  35070  bnj1000  35083  bnj1014  35103  bnj1015  35104  bnj1234  35155  bnj1463  35197  fineqvnttrclse  35268  gblacfnacd  35284  loop1cycl  35319  derangenlem  35353  subfacp1lem3  35364  subfacp1lem5  35366  subfacp1lem6  35367  subfacp1  35368  sconnpht  35411  cnpconn  35412  txpconn  35414  ptpconn  35415  indispconn  35416  connpconn  35417  cvxpconn  35424  cvmliftmo  35466  cvmliftlem14  35479  cvmliftlem15  35480  cvmliftiota  35483  cvmlift2  35498  cvmliftphtlem  35499  cvmlift3lem2  35502  cvmlift3lem6  35506  cvmlift3lem7  35507  cvmlift3lem9  35509  cvmlift3  35510  satfv1lem  35544  satfv1  35545  sategoelfvb  35601  mrsubff1  35696  mrsub0  35698  mrsubccat  35700  mrsubcn  35701  elmsubrn  35710  msubrn  35711  msubco  35713  msubvrs  35742  mclsax  35751  shftvalg  35914  fwddifval  36344  fwddifnval  36345  bj-evalval  37387  unceq  37918  matunitlindflem2  37938  poimirlem17  37958  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  poimirlem27  37968  poimirlem28  37969  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  poimir  37974  broucube  37975  voliunnfl  37985  volsupnfl  37986  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  ftc1anclem2  38015  ftc1anclem5  38018  upixp  38050  fdc  38066  isismty  38122  rrnmval  38149  elghomlem2OLD  38207  isrngohom  38286  islfl  39506  isopos  39626  islaut  40529  ispautN  40545  isldil  40556  isltrn  40565  ltrnid  40581  ltrneq2  40594  isdilN  40600  istrnN  40603  trlval  40608  ltrneq3  40654  cdleme50ex  41005  cdleme  41006  cdlemg1a  41016  ltrniotaval  41027  ltrniotavalbN  41030  cdlemeiota  41031  cdlemg2jlemOLDN  41039  cdlemg2fvlem  41040  cdlemg2klem  41041  istendo  41206  tendoplcbv  41221  tendopl  41222  tendoicbv  41239  tendoi  41240  tendoid0  41271  tendo1ne0  41274  cdlemksv2  41293  cdlemkuv2  41313  cdlemk33N  41355  cdlemk34  41356  cdlemk36  41359  cdlemk19u  41416  cdlemk  41420  tendoex  41421  dvavsca  41463  dvhvscacbv  41544  dvhvscaval  41545  dicopelval  41623  dicelval1sta  41633  diclspsn  41640  dihmeetlem13N  41765  dih1dimatlem0  41774  dih1dimatlem  41775  dihpN  41782  islpolN  41929  hdmap1fval  42242  hdmapfval  42273  sticksstones1  42585  sticksstones2  42586  sticksstones3  42587  sticksstones8  42592  sticksstones10  42594  sticksstones11  42595  sticksstones12a  42596  sticksstones12  42597  sticksstones15  42600  frlmsnic  42985  uvcn0  42987  mplmapghm  42997  evlsvarval  43001  evlsbagval  43002  selvvvval  43018  evlselv  43020  fsuppssindlem2  43025  fsuppssind  43026  prjspnfv01  43057  prjspner01  43058  prjspner1  43059  sn-isghm  43106  ismrc  43133  mzpclval  43157  mzpsubst  43180  mzprename  43181  mzpcompact2lem  43183  eldioph  43190  eldioph2  43194  eldioph2b  43195  eldioph3  43198  rexrabdioph  43222  2rexfrabdioph  43224  3rexfrabdioph  43225  4rexfrabdioph  43226  6rexfrabdioph  43227  7rexfrabdioph  43228  eldioph4i  43240  rabren3dioph  43243  mzpcong  43400  jm2.27dlem1  43437  wepwsolem  43470  aomclem6  43487  aomclem8  43489  dfac11  43490  dgraalem  43573  dgraaub  43576  dgraa0p  43577  mpaaeu  43578  mpaalem  43580  aaitgo  43590  rngunsnply  43597  cantnfresb  43752  tfsconcatun  43765  nvocnvb  43849  eliunov2  44106  rfovcnvfvd  44434  fsovfvd  44437  fsovcnvlem  44440  dssmapfv2d  44445  dssmapnvod  44447  clsk1independent  44473  ntrclskb  44496  ntrclsk13  44498  gneispace2  44559  mnringmulrvald  44654  dvconstbi  44761  addrval  44892  subrval  44893  mulvval  44894  relpeq1  45371  fnchoice  45460  refsum2cnlem1  45468  choicefi  45629  axccdom  45651  fmulcl  46011  fmuldfeqlem1  46012  mccllem  46027  mccl  46028  climf  46052  climf2  46094  dvnprodlem1  46374  dvnprodlem3  46376  dvnprod  46377  stoweidlem2  46430  stoweidlem6  46434  stoweidlem8  46436  stoweidlem9  46437  stoweidlem15  46443  stoweidlem16  46444  stoweidlem17  46445  stoweidlem18  46446  stoweidlem21  46449  stoweidlem27  46455  stoweidlem31  46459  stoweidlem36  46464  stoweidlem37  46465  stoweidlem41  46469  stoweidlem43  46471  stoweidlem44  46472  stoweidlem45  46473  stoweidlem46  46474  stoweidlem48  46476  stoweidlem51  46479  stoweidlem55  46483  stoweidlem59  46487  stoweidlem60  46488  stoweidlem62  46490  fourierdlem2  46537  fourierdlem3  46538  elaa2lem  46661  etransclem11  46673  etransclem24  46686  etransclem26  46688  etransclem28  46690  etransclem35  46697  rrndistlt  46718  ioorrnopn  46733  subsaliuncllem  46785  sge0val  46794  ismea  46879  caragenval  46921  isome  46922  isomenndlem  46958  hoicvrrex  46984  ovnlecvr  46986  ovncvrrp  46992  ovn0lem  46993  ovnsubaddlem1  46998  ovnsubadd  47000  hsphoif  47004  hoidmvval  47005  hsphoival  47007  hoidmvlelem3  47025  hoidmvlelem5  47027  hoidmvle  47028  ovnhoilem1  47029  ovnhoi  47031  ovnlecvr2  47038  ovncvr2  47039  hoidifhspval2  47043  hoiqssbllem2  47051  hspmbllem2  47055  hspmbllem3  47056  hspmbl  47057  ovnovollem1  47084  smfmullem2  47220  smfmul  47223  smfpimcclem  47235  chnerlem1  47312  nthrucw  47316  sinnpoly  47339  cfsetsnfsetfv  47505  cfsetsnfsetfo  47508  iccpart  47876  iccpartiun  47894  icceuelpart  47896  nnsum3primes4  48264  nnsum3primesgbe  48268  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  bgoldbtbnd  48285  isisubgr  48338  isgrim  48358  grimidvtxedg  48361  grimcnv  48364  grimco  48365  isuspgrim0  48370  gricushgr  48393  ushggricedg  48403  uhgrimisgrgric  48407  isgrtri  48419  isubgr3stgrlem3  48444  isubgr3stgr  48451  isgrlim  48458  uspgrlim  48468  grlicref  48488  grlicsym  48489  grlictr  48491  grlimedgnedg  48607  isupwlk  48612  lincval  48885  lincdifsn  48900  linindslinci  48924  lindslinindsimp1  48933  linds0  48941  el0ldep  48942  lindsrng01  48944  snlindsntorlem  48946  ldepspr  48949  islindeps2  48959  zlmodzxzldep  48980  bigoval  49025  elbigo  49027  0aryfvalelfv  49111  1arympt1fv  49115  1arymaptfv  49116  1arymaptfo  49119  2arymptfv  49126  2arymaptfv  49127  2arymaptfo  49130  prelrrx2b  49190  rrx2plord  49196  rrx2vlinest  49217  rrx2linesl  49219  elrrx2linest2  49221  line2ylem  49227  line2xlem  49229  itsclc0  49247  itsclc0b  49248  itscnhlinecirc02p  49261  elfvne0  49324  iinfprg  49534  thincciso  49928  thinccisod  49929  setrecseq  50160  aacllem  50276