Theorem fveq1 6896

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 5150	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6532	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6556	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6556	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2793	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1534   class class class wbr 5148  ℩cio 6498  ‘cfv 6548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ss 3964  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556

This theorem is referenced by:  fveq1i  6898  fveq1d  6899  iffv  6914  fvmptd3f  7020  fvmptdv2  7023  eqfnun  7046  fsnex  7292  f1prex  7293  isoeq1  7325  oveq  7426  elovmpt3imp  7678  ofrfvalg  7693  offval  7694  offval3  7986  bropopvvv  8095  bropfvvvvlem  8096  poseq  8163  soseq  8164  frrlem1  8292  frrlem13  8304  wfrlem1OLD  8329  wfrlem3OLDa  8332  wfrlem15OLD  8344  smoeq  8371  tfrlem12  8410  tz7.44-2  8428  tz7.44-3  8429  rdgeq1  8432  fsetfocdm  8880  fsetprcnex  8881  mapsncnv  8912  elixp2  8920  resixpfo  8955  elixpsn  8956  mapsnend  9061  enfixsn  9106  mapxpen  9168  ac6sfi  9312  ordtypelem7  9548  wemaplem1  9570  ixpiunwdom  9614  oemapval  9707  cantnf  9717  wemapwe  9721  cnfcom3clem  9729  ssttrcl  9739  ttrcltr  9740  ttrclss  9744  ttrclselem2  9750  updjud  9958  infxpenc2lem2  10044  fseqenlem1  10048  dfac8clem  10056  ac5num  10060  acni  10069  acni2  10070  acnlem  10072  dfac4  10146  dfac5lem5  10151  dfac2a  10153  dfac9  10160  dfacacn  10165  dfac12lem1  10167  dfac12r  10170  cofsmo  10293  cfsmolem  10294  cfsmo  10295  cfcoflem  10296  coftr  10297  alephsing  10300  isfin3ds  10353  fin23lem17  10362  fin23lem32  10368  fin23lem39  10374  isf33lem  10390  isf34lem6  10404  axcc2lem  10460  axcc3  10462  axdc2lem  10472  axdc3lem2  10475  axdc3lem3  10476  axdc3  10478  axdc4lem  10479  axcclem  10481  ac6num  10503  axdclem2  10544  konigthlem  10592  inar1  10799  1fv  13653  axdc4uzlem  13981  seqeq3  14004  seqof  14057  ccatfval  14556  wrdl1s1  14597  ccat1st1st  14611  cshf1  14793  cshweqrep  14804  wrdlen2i  14926  wwlktovf  14940  wwlktovf1  14941  wwlktovfo  14942  wrd2f1tovbij  14944  rtrclreclem1  15037  dfrtrclrec2  15038  rtrclreclem2  15039  rtrclreclem4  15041  dfrtrcl2  15042  clim  15471  rlim  15472  ello1  15492  elo1  15503  summo  15696  fsum  15699  prodmo  15913  fprod  15918  bpolylem  16025  bpolyval  16026  vdwlem6  16955  vdwlem8  16957  ramcl  16998  strfvnd  17154  prdsplusgval  17455  prdsmulrval  17457  prdsleval  17459  prdsdsval  17460  prdsvscaval  17461  xpsff1o  17549  isacs2  17633  isnat  17937  yonedalem3b  18271  yonedainv  18273  ismgmhm  18656  ismhm  18742  prdspjmhm  18781  isgrpinv  18950  pwsmulg  19074  isghm  19170  cayleylem2  19368  symgfix2  19371  gsmsymgrfix  19383  gsmsymgreq  19387  symgfixelq  19388  pmtr3ncomlem2  19429  pmtrdifel  19435  pmtrdifwrdel  19440  pmtrdifwrdel2  19441  psgnunilem2  19450  psgnunilem3  19451  efgsdm  19685  efgredlemd  19699  efgredlem  19702  efgred  19703  efgrelexlema  19704  efgrelexlemb  19705  prdsgsum  19936  pwspjmhmmgpd  20264  pwsexpg  20265  isrnghm  20380  isabv  20699  islmhm  20912  frgpcyg  21507  psgndiflemB  21532  psgndiflemA  21533  dsmmelbas  21673  frlmipval  21713  frlmphl  21715  uvcf1  21726  islindf  21746  islindf4  21772  psrmulfval  21886  evlslem2  22025  evlslem3  22026  evlslem1  22028  mpfrcl  22031  selvval  22061  psdval  22083  psdcoef  22084  psdadd  22087  psdmul  22090  coe1fval  22124  coe1mul2lem2  22187  coe1tm  22192  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  23154  1stcfb  23362  ptpjpre1  23488  elpt  23489  elptr  23490  ptpjopn  23529  dfac14  23535  upxp  23540  pthaus  23555  ptrescn  23556  xkoptsub  23571  cnmptkp  23597  xkofvcn  23601  cnmptk1p  23602  cnmptk2  23603  ptunhmeo  23725  ptcmplem3  23971  ptcmplem4  23972  symgtgp  24023  prdstmdd  24041  isucn  24196  imasdsf1olem  24292  prdsxmslem2  24451  tngngp3  24586  nmoval  24645  elcncf  24822  ishtpy  24911  pcoval  24951  om1elbas  24972  elpi1i  24986  iscau  25217  rrxds  25334  rrxdsfival  25354  ehl1eudisval  25362  ehl2eudisval  25364  mbfi1fseqlem6  25663  mbfi1flimlem  25665  isibl  25708  deg1ldg  26041  deg1leb  26044  elply2  26143  elplyr  26148  ne0p  26154  coeeu  26172  coelem  26173  coeeq  26174  coeidlem  26184  elqaalem3  26269  qaa  26271  iaa  26273  aareccl  26274  aannenlem2  26277  aaliou2  26288  dchrptlem2  27211  dchrpt  27213  dchrsum2  27214  sumdchr2  27216  dchrvmaeq0  27450  rpvmasum2  27458  dchrisum0re  27459  ostth  27585  sltval  27593  nolesgn2o  27617  nogesgn1o  27619  noresle  27643  nosupprefixmo  27646  noinfprefixmo  27647  nosupcbv  27648  nosupfv  27652  noinfcbv  27663  noinffv  27667  iscgrg  28329  isismt  28351  israg  28514  iseqlg  28684  brbtwn  28723  brbtwn2  28729  colinearalg  28734  axsegconlem1  28741  axsegcon  28751  ax5seglem5  28757  axpasch  28765  axlowdim  28785  axeuclidlem  28786  axcontlem1  28788  axcontlem2  28789  axcontlem5  28792  vtxdgfval  29294  1egrvtxdg1  29336  isewlk  29429  iswlk  29437  uspgr2wlkeq2  29474  iswlkon  29484  isclwlk  29600  iscrct  29617  iscycl  29618  iswwlks  29660  wwlknon  29681  wlkiswwlks2  29699  wwlksnredwwlkn0  29720  wlksnwwlknvbij  29732  wwlksnextproplem3  29735  wwlksnextprop  29736  umgr2wlk  29773  midwwlks2s3  29776  elwwlks2  29790  elwspths2spth  29791  rusgrnumwwlkslem  29793  rusgrnumwwlkb0  29795  rusgrnumwwlks  29798  isclwwlk  29807  clwlkclwwlklem1  29822  clwwlkn1loopb  29866  clwwlkel  29869  clwwlkf  29870  clwwlkf1  29872  isclwwlknon  29914  clwwlknon1  29920  s2elclwwlknon2  29927  clwwlkvbij  29936  uhgr3cyclex  30005  fusgreg2wsplem  30156  fusgr2wsp2nb  30157  fusgreghash2wsp  30161  2clwwlkel  30172  extwwlkfabel  30176  numclwwlk1lem2fv  30179  numclwwlk1lem2  30183  clwwlknonclwlknonf1o  30185  dlwwlknondlwlknonf1o  30188  numclwwlk2lem1  30199  numclwlk2lem2f  30200  numclwlk2lem2f1o  30202  ex-fv  30266  isnvlem  30433  islno  30576  nmooval  30586  nmblolbi  30623  isphg  30640  ajmoi  30681  ajval  30684  ubthlem3  30695  htthlem  30740  hcau  31007  hlimi  31011  hosmval  31558  hommval  31559  hodmval  31560  hfsmval  31561  hfmmval  31562  adjmo  31655  nmopval  31679  elcnop  31680  ellnop  31681  elunop  31695  elhmop  31696  nmfnval  31699  elcnfn  31705  ellnfn  31706  adjeu  31712  adjval  31713  eigvecval  31719  eigvalfval  31720  adj1  31756  adjeq  31758  hmopadj2  31764  lnopeq0i  31830  lnopeq  31832  elunop2  31836  lnophm  31842  hmopco  31846  nmbdoplb  31848  nmcoplb  31853  lnopcon  31858  lnfn0  31870  lnfnmul  31871  nmbdfnlb  31873  nmcfnlb  31877  lnfncon  31879  riesz4  31887  riesz1  31888  cnlnadjlem9  31898  cnlnadjeu  31901  cnlnssadj  31903  nmopcoi  31918  bra11  31931  cnvbraval  31933  pjss2coi  31987  pjssdif2i  31997  pjssdif1i  31998  pjclem4  32022  pj3si  32030  pj3cor1i  32032  isst  32036  ishst  32037  stri  32080  hstri  32088  aciunf1lem  32461  ismnt  32723  mgcval  32727  linds2eq  33109  elrspunidl  33157  elrspunsn  33158  lbsdiflsp0  33324  fedgmullem1  33327  fedgmullem2  33328  fedgmul  33329  lmatval  33414  mdetpmtr1  33424  zarcmplem  33482  ismeas  33818  isrnmeas  33819  cntnevol  33847  carsgval  33923  sitgval  33952  eulerpartleme  33983  eulerpartlemd  33986  eulerpartlemr  33994  eulerpartlemgvv  33996  eulerpart  34002  cndprobval  34053  signstfvneq0  34204  reprsum  34245  reprsuc  34247  reprpmtf1o  34258  reprdifc  34259  breprexp  34265  vtsval  34269  hgt750lemb  34288  hgt750lema  34289  hgt750leme  34290  bnj66  34491  bnj106  34499  bnj125  34503  bnj154  34509  bnj155  34510  bnj526  34519  bnj540  34523  bnj609  34548  bnj611  34549  bnj893  34559  bnj1000  34572  bnj1014  34592  bnj1015  34593  bnj1234  34644  bnj1463  34686  loop1cycl  34747  derangenlem  34781  subfacp1lem3  34792  subfacp1lem5  34794  subfacp1lem6  34795  subfacp1  34796  sconnpht  34839  cnpconn  34840  txpconn  34842  ptpconn  34843  indispconn  34844  connpconn  34845  cvxpconn  34852  cvmliftmo  34894  cvmliftlem14  34907  cvmliftlem15  34908  cvmliftiota  34911  cvmlift2  34926  cvmliftphtlem  34927  cvmlift3lem2  34930  cvmlift3lem6  34934  cvmlift3lem7  34935  cvmlift3lem9  34937  cvmlift3  34938  satfv1lem  34972  satfv1  34973  sategoelfvb  35029  mrsubff1  35124  mrsub0  35126  mrsubccat  35128  mrsubcn  35129  elmsubrn  35138  msubrn  35139  msubco  35141  msubvrs  35170  mclsax  35179  shftvalg  35326  fwddifval  35758  fwddifnval  35759  bj-evalval  36554  unceq  37070  matunitlindflem2  37090  poimirlem17  37110  poimirlem20  37113  poimirlem22  37115  poimirlem23  37116  poimirlem27  37120  poimirlem28  37121  poimirlem30  37123  poimirlem31  37124  poimirlem32  37125  poimir  37126  broucube  37127  voliunnfl  37137  volsupnfl  37138  itg2addnclem  37144  itg2addnclem3  37146  itg2addnc  37147  ftc1anclem2  37167  ftc1anclem5  37170  upixp  37202  fdc  37218  isismty  37274  rrnmval  37301  elghomlem2OLD  37359  isrngohom  37438  islfl  38532  isopos  38652  islaut  39556  ispautN  39572  isldil  39583  isltrn  39592  ltrnid  39608  ltrneq2  39621  isdilN  39627  istrnN  39630  trlval  39635  ltrneq3  39681  cdleme50ex  40032  cdleme  40033  cdlemg1a  40043  ltrniotaval  40054  ltrniotavalbN  40057  cdlemeiota  40058  cdlemg2jlemOLDN  40066  cdlemg2fvlem  40067  cdlemg2klem  40068  istendo  40233  tendoplcbv  40248  tendopl  40249  tendoicbv  40266  tendoi  40267  tendoid0  40298  tendo1ne0  40301  cdlemksv2  40320  cdlemkuv2  40340  cdlemk33N  40382  cdlemk34  40383  cdlemk36  40386  cdlemk19u  40443  cdlemk  40447  tendoex  40448  dvavsca  40490  dvhvscacbv  40571  dvhvscaval  40572  dicopelval  40650  dicelval1sta  40660  diclspsn  40667  dihmeetlem13N  40792  dih1dimatlem0  40801  dih1dimatlem  40802  dihpN  40809  islpolN  40956  hdmap1fval  41269  hdmapfval  41300  sticksstones1  41618  sticksstones2  41619  sticksstones3  41620  sticksstones8  41625  sticksstones10  41627  sticksstones11  41628  sticksstones12a  41629  sticksstones12  41630  sticksstones15  41633  frlmsnic  41770  uvcn0  41772  pwsgprod  41774  mplmapghm  41789  evlsvval  41793  evlsvvval  41796  evlsvarval  41798  evlsbagval  41799  selvvvval  41818  evlselv  41820  fsuppssindlem2  41825  fsuppssind  41826  prjspnfv01  42048  prjspner01  42049  prjspner1  42050  ismrc  42121  mzpclval  42145  mzpsubst  42168  mzprename  42169  mzpcompact2lem  42171  eldioph  42178  eldioph2  42182  eldioph2b  42183  eldioph3  42186  rexrabdioph  42214  2rexfrabdioph  42216  3rexfrabdioph  42217  4rexfrabdioph  42218  6rexfrabdioph  42219  7rexfrabdioph  42220  eldioph4i  42232  rabren3dioph  42235  mzpcong  42393  jm2.27dlem1  42430  wepwsolem  42466  aomclem6  42483  aomclem8  42485  dfac11  42486  dgraalem  42569  dgraaub  42572  dgraa0p  42573  mpaaeu  42574  mpaalem  42576  aaitgo  42586  rngunsnply  42597  cantnfresb  42753  tfsconcatun  42766  nvocnvb  42852  eliunov2  43109  rfovcnvfvd  43437  fsovfvd  43440  fsovcnvlem  43443  dssmapfv2d  43448  dssmapnvod  43450  clsk1independent  43476  ntrclskb  43499  ntrclsk13  43501  gneispace2  43562  mnringmulrvald  43664  dvconstbi  43771  addrval  43903  subrval  43904  mulvval  43905  fnchoice  44391  refsum2cnlem1  44399  choicefi  44573  axccdom  44595  fmulcl  44969  fmuldfeqlem1  44970  mccllem  44985  mccl  44986  climf  45010  climf2  45054  dvnprodlem1  45334  dvnprodlem3  45336  dvnprod  45337  stoweidlem2  45390  stoweidlem6  45394  stoweidlem8  45396  stoweidlem9  45397  stoweidlem15  45403  stoweidlem16  45404  stoweidlem17  45405  stoweidlem18  45406  stoweidlem21  45409  stoweidlem27  45415  stoweidlem31  45419  stoweidlem36  45424  stoweidlem37  45425  stoweidlem41  45429  stoweidlem43  45431  stoweidlem44  45432  stoweidlem45  45433  stoweidlem46  45434  stoweidlem48  45436  stoweidlem51  45439  stoweidlem55  45443  stoweidlem59  45447  stoweidlem60  45448  stoweidlem62  45450  fourierdlem2  45497  fourierdlem3  45498  elaa2lem  45621  etransclem11  45633  etransclem24  45646  etransclem26  45648  etransclem28  45650  etransclem35  45657  rrndistlt  45678  ioorrnopn  45693  subsaliuncllem  45745  sge0val  45754  ismea  45839  caragenval  45881  isome  45882  isomenndlem  45918  hoicvrrex  45944  ovnlecvr  45946  ovncvrrp  45952  ovn0lem  45953  ovnsubaddlem1  45958  ovnsubadd  45960  hsphoif  45964  hoidmvval  45965  hsphoival  45967  hoidmvlelem3  45985  hoidmvlelem5  45987  hoidmvle  45988  ovnhoilem1  45989  ovnhoi  45991  ovnlecvr2  45998  ovncvr2  45999  hoidifhspval2  46003  hoiqssbllem2  46011  hspmbllem2  46015  hspmbllem3  46016  hspmbl  46017  ovnovollem1  46044  smfmullem2  46180  smfmul  46183  smfpimcclem  46195  tworepnotupword  46272  cfsetsnfsetfv  46439  cfsetsnfsetfo  46442  iccpart  46756  iccpartiun  46774  icceuelpart  46776  nnsum3primes4  47128  nnsum3primesgbe  47132  nnsum4primesodd  47136  nnsum4primesoddALTV  47137  nnsum4primeseven  47140  nnsum4primesevenALTV  47141  bgoldbtbnd  47149  isgrim  47166  isuspgrim0  47170  grimidvtxedg  47174  grimcnv  47177  grimco  47178  gricushgr  47183  ushggricedg  47193  isupwlk  47198  lincval  47477  lincdifsn  47492  linindslinci  47516  lindslinindsimp1  47525  linds0  47533  el0ldep  47534  lindsrng01  47536  snlindsntorlem  47538  ldepspr  47541  islindeps2  47551  zlmodzxzldep  47572  bigoval  47622  elbigo  47624  0aryfvalelfv  47708  1arympt1fv  47712  1arymaptfv  47713  1arymaptfo  47716  2arymptfv  47723  2arymaptfv  47724  2arymaptfo  47727  prelrrx2b  47787  rrx2plord  47793  rrx2vlinest  47814  rrx2linesl  47816  elrrx2linest2  47818  line2ylem  47824  line2xlem  47826  itsclc0  47844  itsclc0b  47845  itscnhlinecirc02p  47858  elfvne0  47901  thincciso  48055  setrecseq  48116  aacllem  48234