Theorem fveq1 6831

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 5098	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6474	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6498	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6498	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2794	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5096  ℩cio 6444  ‘cfv 6490

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498

This theorem is referenced by:  fveq1i  6833  fveq1d  6834  iffv  6849  fvmptd3f  6954  fvmptdv2  6957  eqfnun  6980  fsnex  7227  f1prex  7228  isoeq1  7261  oveq  7362  elovmpt3imp  7613  ofrfvalg  7628  offval  7629  offval3  7924  bropopvvv  8030  bropfvvvvlem  8031  poseq  8098  soseq  8099  frrlem1  8226  frrlem13  8238  smoeq  8280  tfrlem12  8318  tz7.44-2  8336  tz7.44-3  8337  rdgeq1  8340  fsetfocdm  8796  fsetprcnex  8797  mapsncnv  8829  elixp2  8837  resixpfo  8872  elixpsn  8873  mapsnend  8971  enfixsn  9012  mapxpen  9069  ac6sfi  9182  ordtypelem7  9427  wemaplem1  9449  ixpiunwdom  9493  oemapval  9590  cantnf  9600  wemapwe  9604  cnfcom3clem  9612  ssttrcl  9622  ttrcltr  9623  ttrclss  9627  ttrclselem2  9633  updjud  9844  infxpenc2lem2  9928  fseqenlem1  9932  dfac8clem  9940  ac5num  9944  acni  9953  acni2  9954  acnlem  9956  dfac4  10030  dfac5lem5  10035  dfac2a  10038  dfac9  10045  dfacacn  10050  dfac12lem1  10052  dfac12r  10055  cofsmo  10177  cfsmolem  10178  cfsmo  10179  cfcoflem  10180  coftr  10181  alephsing  10184  isfin3ds  10237  fin23lem17  10246  fin23lem32  10252  fin23lem39  10258  isf33lem  10274  isf34lem6  10288  axcc2lem  10344  axcc3  10346  axdc2lem  10356  axdc3lem2  10359  axdc3lem3  10360  axdc3  10362  axdc4lem  10363  axcclem  10365  ac6num  10387  axdclem2  10428  konigthlem  10477  inar1  10684  1fv  13561  axdc4uzlem  13904  seqeq3  13927  seqof  13980  ccatfval  14494  wrdl1s1  14536  ccat1st1st  14550  cshf1  14731  cshweqrep  14742  wrdlen2i  14863  wwlktovf  14877  wwlktovf1  14878  wwlktovfo  14879  wrd2f1tovbij  14881  rtrclreclem1  14978  dfrtrclrec2  14979  rtrclreclem2  14980  rtrclreclem4  14982  dfrtrcl2  14983  clim  15415  rlim  15416  ello1  15436  elo1  15447  summo  15638  fsum  15641  prodmo  15857  fprod  15862  bpolylem  15969  bpolyval  15970  vdwlem6  16912  vdwlem8  16914  ramcl  16955  strfvnd  17110  prdsplusgval  17391  prdsmulrval  17393  prdsleval  17395  prdsdsval  17396  prdsvscaval  17397  xpsff1o  17486  isacs2  17574  isnat  17872  yonedalem3b  18200  yonedainv  18202  ischn  18528  chnind  18542  chnub  18543  ismgmhm  18619  ismhm  18708  prdspjmhm  18752  isgrpinv  18921  pwsmulg  19047  isghm  19142  isghmOLD  19143  cayleylem2  19340  symgfix2  19343  gsmsymgrfix  19355  gsmsymgreq  19359  symgfixelq  19360  pmtr3ncomlem2  19401  pmtrdifel  19407  pmtrdifwrdel  19412  pmtrdifwrdel2  19413  psgnunilem2  19422  psgnunilem3  19423  efgsdm  19657  efgredlemd  19671  efgredlem  19674  efgred  19675  efgrelexlema  19676  efgrelexlemb  19677  prdsgsum  19908  pwspjmhmmgpd  20261  pwsexpg  20262  pwsgprod  20263  isrnghm  20375  isabv  20742  islmhm  20977  frgpcyg  21526  psgndiflemB  21553  psgndiflemA  21554  dsmmelbas  21692  frlmipval  21732  frlmphl  21734  uvcf1  21745  islindf  21765  islindf4  21791  psrmulfval  21897  evlslem2  22032  evlslem3  22033  evlslem1  22035  mpfrcl  22038  evlsvval  22043  evlsvvval  22046  selvval  22076  psdval  22100  psdcoef  22101  psdadd  22104  psdmul  22107  psdmvr  22110  coe1fval  22144  coe1mul2lem2  22208  coe1tm  22213  madetsumid  22403  mvmulval  22485  marepvval0  22508  mulmarep1gsum2  22516  mdetleib2  22530  m1detdiag  22539  mdetralt  22550  mdetunilem7  22560  mdetunilem9  22562  m2detleiblem3  22571  m2detleiblem4  22572  m2detleib  22573  symgmatr01lem  22595  gsummatr01lem1  22597  gsummatr01lem4  22600  gsummatr01  22601  smadiadetlem3  22610  pmatcoe1fsupp  22643  pmatcollpw3lem  22725  pmatcollpw3fi1lem2  22729  iscnp  23179  1stcfb  23387  ptpjpre1  23513  elpt  23514  elptr  23515  ptpjopn  23554  dfac14  23560  upxp  23565  pthaus  23580  ptrescn  23581  xkoptsub  23596  cnmptkp  23622  xkofvcn  23626  cnmptk1p  23627  cnmptk2  23628  ptunhmeo  23750  ptcmplem3  23996  ptcmplem4  23997  symgtgp  24048  prdstmdd  24066  isucn  24219  imasdsf1olem  24315  prdsxmslem2  24471  tngngp3  24598  nmoval  24657  elcncf  24836  ishtpy  24925  pcoval  24965  om1elbas  24986  elpi1i  25000  iscau  25230  rrxds  25347  rrxdsfival  25367  ehl1eudisval  25375  ehl2eudisval  25377  mbfi1fseqlem6  25675  mbfi1flimlem  25677  isibl  25720  deg1ldg  26051  deg1leb  26054  elply2  26155  elplyr  26160  ne0p  26166  coeeu  26184  coelem  26185  coeeq  26186  coeidlem  26196  elqaalem3  26283  qaa  26285  iaa  26287  aareccl  26288  aannenlem2  26291  aaliou2  26302  dchrptlem2  27230  dchrpt  27232  dchrsum2  27233  sumdchr2  27235  dchrvmaeq0  27469  rpvmasum2  27477  dchrisum0re  27478  ostth  27604  sltval  27613  nolesgn2o  27637  nogesgn1o  27639  noresle  27663  nosupprefixmo  27666  noinfprefixmo  27667  nosupcbv  27668  nosupfv  27672  noinfcbv  27683  noinffv  27687  iscgrg  28533  isismt  28555  israg  28718  iseqlg  28888  brbtwn  28921  brbtwn2  28927  colinearalg  28932  axsegconlem1  28939  axsegcon  28949  ax5seglem5  28955  axpasch  28963  axlowdim  28983  axeuclidlem  28984  axcontlem1  28986  axcontlem2  28987  axcontlem5  28990  vtxdgfval  29490  1egrvtxdg1  29532  isewlk  29625  iswlk  29633  uspgr2wlkeq2  29669  iswlkon  29678  isclwlk  29795  iscrct  29812  iscycl  29813  iswwlks  29858  wwlknon  29879  wlkiswwlks2  29897  wwlksnredwwlkn0  29918  wlksnwwlknvbij  29930  wwlksnextproplem3  29933  wwlksnextprop  29934  umgr2wlk  29971  midwwlks2s3  29974  elwwlks2  29991  elwspths2spth  29992  rusgrnumwwlkslem  29994  rusgrnumwwlkb0  29996  rusgrnumwwlks  29999  isclwwlk  30008  clwlkclwwlklem1  30023  clwwlkn1loopb  30067  clwwlkel  30070  clwwlkf  30071  clwwlkf1  30073  isclwwlknon  30115  clwwlknon1  30121  s2elclwwlknon2  30128  clwwlkvbij  30137  uhgr3cyclex  30206  fusgreg2wsplem  30357  fusgr2wsp2nb  30358  fusgreghash2wsp  30362  2clwwlkel  30373  extwwlkfabel  30377  numclwwlk1lem2fv  30380  numclwwlk1lem2  30384  clwwlknonclwlknonf1o  30386  dlwwlknondlwlknonf1o  30389  numclwwlk2lem1  30400  numclwlk2lem2f  30401  numclwlk2lem2f1o  30403  ex-fv  30467  isnvlem  30634  islno  30777  nmooval  30787  nmblolbi  30824  isphg  30841  ajmoi  30882  ajval  30885  ubthlem3  30896  htthlem  30941  hcau  31208  hlimi  31212  hosmval  31759  hommval  31760  hodmval  31761  hfsmval  31762  hfmmval  31763  adjmo  31856  nmopval  31880  elcnop  31881  ellnop  31882  elunop  31896  elhmop  31897  nmfnval  31900  elcnfn  31906  ellnfn  31907  adjeu  31913  adjval  31914  eigvecval  31920  eigvalfval  31921  adj1  31957  adjeq  31959  hmopadj2  31965  lnopeq0i  32031  lnopeq  32033  elunop2  32037  lnophm  32043  hmopco  32047  nmbdoplb  32049  nmcoplb  32054  lnopcon  32059  lnfn0  32071  lnfnmul  32072  nmbdfnlb  32074  nmcfnlb  32078  lnfncon  32080  riesz4  32088  riesz1  32089  cnlnadjlem9  32099  cnlnadjeu  32102  cnlnssadj  32104  nmopcoi  32119  bra11  32132  cnvbraval  32134  pjss2coi  32188  pjssdif2i  32198  pjssdif1i  32199  pjclem4  32223  pj3si  32231  pj3cor1i  32233  isst  32237  ishst  32238  stri  32281  hstri  32289  aciunf1lem  32689  ismnt  33014  mgcval  33018  fzo0pmtrlast  33123  elrgspnlem1  33273  elrgspnlem2  33274  elrgspnlem3  33275  elrgspnlem4  33276  elrgspn  33277  elrgspnsubrunlem1  33278  linds2eq  33411  elrspunidl  33458  elrspunsn  33459  dfufd2lem  33579  extvfv  33647  extvfvv  33648  extvfvcl  33650  evlvarval  33655  evlextv  33656  mplvrpmga  33659  splysubrg  33667  issply  33668  vietalem  33684  vieta  33685  lbsdiflsp0  33732  fedgmullem1  33735  fedgmullem2  33736  fedgmul  33737  fldextrspunlsplem  33779  fldextrspunlsp  33780  fldext2chn  33834  constrextdg2lem  33854  constrextdg2  33855  lmatval  33919  mdetpmtr1  33929  zarcmplem  33987  ismeas  34305  isrnmeas  34306  cntnevol  34334  carsgval  34409  sitgval  34438  eulerpartleme  34469  eulerpartlemd  34472  eulerpartlemr  34480  eulerpartlemgvv  34482  eulerpart  34488  cndprobval  34539  signstfvneq0  34678  reprsum  34719  reprsuc  34721  reprpmtf1o  34732  reprdifc  34733  breprexp  34739  vtsval  34743  hgt750lemb  34762  hgt750lema  34763  hgt750leme  34764  bnj66  34965  bnj106  34973  bnj125  34977  bnj154  34983  bnj155  34984  bnj526  34993  bnj540  34997  bnj609  35022  bnj611  35023  bnj893  35033  bnj1000  35046  bnj1014  35066  bnj1015  35067  bnj1234  35118  bnj1463  35160  fineqvnttrclse  35229  gblacfnacd  35245  loop1cycl  35280  derangenlem  35314  subfacp1lem3  35325  subfacp1lem5  35327  subfacp1lem6  35328  subfacp1  35329  sconnpht  35372  cnpconn  35373  txpconn  35375  ptpconn  35376  indispconn  35377  connpconn  35378  cvxpconn  35385  cvmliftmo  35427  cvmliftlem14  35440  cvmliftlem15  35441  cvmliftiota  35444  cvmlift2  35459  cvmliftphtlem  35460  cvmlift3lem2  35463  cvmlift3lem6  35467  cvmlift3lem7  35468  cvmlift3lem9  35470  cvmlift3  35471  satfv1lem  35505  satfv1  35506  sategoelfvb  35562  mrsubff1  35657  mrsub0  35659  mrsubccat  35661  mrsubcn  35662  elmsubrn  35671  msubrn  35672  msubco  35674  msubvrs  35703  mclsax  35712  shftvalg  35875  fwddifval  36305  fwddifnval  36306  bj-evalval  37219  unceq  37737  matunitlindflem2  37757  poimirlem17  37777  poimirlem20  37780  poimirlem22  37782  poimirlem23  37783  poimirlem27  37787  poimirlem28  37788  poimirlem30  37790  poimirlem31  37791  poimirlem32  37792  poimir  37793  broucube  37794  voliunnfl  37804  volsupnfl  37805  itg2addnclem  37811  itg2addnclem3  37813  itg2addnc  37814  ftc1anclem2  37834  ftc1anclem5  37837  upixp  37869  fdc  37885  isismty  37941  rrnmval  37968  elghomlem2OLD  38026  isrngohom  38105  islfl  39259  isopos  39379  islaut  40282  ispautN  40298  isldil  40309  isltrn  40318  ltrnid  40334  ltrneq2  40347  isdilN  40353  istrnN  40356  trlval  40361  ltrneq3  40407  cdleme50ex  40758  cdleme  40759  cdlemg1a  40769  ltrniotaval  40780  ltrniotavalbN  40783  cdlemeiota  40784  cdlemg2jlemOLDN  40792  cdlemg2fvlem  40793  cdlemg2klem  40794  istendo  40959  tendoplcbv  40974  tendopl  40975  tendoicbv  40992  tendoi  40993  tendoid0  41024  tendo1ne0  41027  cdlemksv2  41046  cdlemkuv2  41066  cdlemk33N  41108  cdlemk34  41109  cdlemk36  41112  cdlemk19u  41169  cdlemk  41173  tendoex  41174  dvavsca  41216  dvhvscacbv  41297  dvhvscaval  41298  dicopelval  41376  dicelval1sta  41386  diclspsn  41393  dihmeetlem13N  41518  dih1dimatlem0  41527  dih1dimatlem  41528  dihpN  41535  islpolN  41682  hdmap1fval  41995  hdmapfval  42026  sticksstones1  42339  sticksstones2  42340  sticksstones3  42341  sticksstones8  42346  sticksstones10  42348  sticksstones11  42349  sticksstones12a  42350  sticksstones12  42351  sticksstones15  42354  frlmsnic  42737  uvcn0  42739  mplmapghm  42749  evlsvarval  42753  evlsbagval  42754  selvvvval  42770  evlselv  42772  fsuppssindlem2  42777  fsuppssind  42778  prjspnfv01  42809  prjspner01  42810  prjspner1  42811  sn-isghm  42858  ismrc  42885  mzpclval  42909  mzpsubst  42932  mzprename  42933  mzpcompact2lem  42935  eldioph  42942  eldioph2  42946  eldioph2b  42947  eldioph3  42950  rexrabdioph  42978  2rexfrabdioph  42980  3rexfrabdioph  42981  4rexfrabdioph  42982  6rexfrabdioph  42983  7rexfrabdioph  42984  eldioph4i  42996  rabren3dioph  42999  mzpcong  43156  jm2.27dlem1  43193  wepwsolem  43226  aomclem6  43243  aomclem8  43245  dfac11  43246  dgraalem  43329  dgraaub  43332  dgraa0p  43333  mpaaeu  43334  mpaalem  43336  aaitgo  43346  rngunsnply  43353  cantnfresb  43508  tfsconcatun  43521  nvocnvb  43605  eliunov2  43862  rfovcnvfvd  44190  fsovfvd  44193  fsovcnvlem  44196  dssmapfv2d  44201  dssmapnvod  44203  clsk1independent  44229  ntrclskb  44252  ntrclsk13  44254  gneispace2  44315  mnringmulrvald  44410  dvconstbi  44517  addrval  44648  subrval  44649  mulvval  44650  relpeq1  45127  fnchoice  45216  refsum2cnlem1  45224  choicefi  45386  axccdom  45408  fmulcl  45769  fmuldfeqlem1  45770  mccllem  45785  mccl  45786  climf  45810  climf2  45852  dvnprodlem1  46132  dvnprodlem3  46134  dvnprod  46135  stoweidlem2  46188  stoweidlem6  46192  stoweidlem8  46194  stoweidlem9  46195  stoweidlem15  46201  stoweidlem16  46202  stoweidlem17  46203  stoweidlem18  46204  stoweidlem21  46207  stoweidlem27  46213  stoweidlem31  46217  stoweidlem36  46222  stoweidlem37  46223  stoweidlem41  46227  stoweidlem43  46229  stoweidlem44  46230  stoweidlem45  46231  stoweidlem46  46232  stoweidlem48  46234  stoweidlem51  46237  stoweidlem55  46241  stoweidlem59  46245  stoweidlem60  46246  stoweidlem62  46248  fourierdlem2  46295  fourierdlem3  46296  elaa2lem  46419  etransclem11  46431  etransclem24  46444  etransclem26  46446  etransclem28  46448  etransclem35  46455  rrndistlt  46476  ioorrnopn  46491  subsaliuncllem  46543  sge0val  46552  ismea  46637  caragenval  46679  isome  46680  isomenndlem  46716  hoicvrrex  46742  ovnlecvr  46744  ovncvrrp  46750  ovn0lem  46751  ovnsubaddlem1  46756  ovnsubadd  46758  hsphoif  46762  hoidmvval  46763  hsphoival  46765  hoidmvlelem3  46783  hoidmvlelem5  46785  hoidmvle  46786  ovnhoilem1  46787  ovnhoi  46789  ovnlecvr2  46796  ovncvr2  46797  hoidifhspval2  46801  hoiqssbllem2  46809  hspmbllem2  46813  hspmbllem3  46814  hspmbl  46815  ovnovollem1  46842  smfmullem2  46978  smfmul  46981  smfpimcclem  46993  chnerlem1  47068  nthrucw  47072  sinnpoly  47079  cfsetsnfsetfv  47245  cfsetsnfsetfo  47248  iccpart  47604  iccpartiun  47622  icceuelpart  47624  nnsum3primes4  47976  nnsum3primesgbe  47980  nnsum4primesodd  47984  nnsum4primesoddALTV  47985  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  bgoldbtbnd  47997  isisubgr  48050  isgrim  48070  grimidvtxedg  48073  grimcnv  48076  grimco  48077  isuspgrim0  48082  gricushgr  48105  ushggricedg  48115  uhgrimisgrgric  48119  isgrtri  48131  isubgr3stgrlem3  48156  isubgr3stgr  48163  isgrlim  48170  uspgrlim  48180  grlicref  48200  grlicsym  48201  grlictr  48203  grlimedgnedg  48319  isupwlk  48324  lincval  48597  lincdifsn  48612  linindslinci  48636  lindslinindsimp1  48645  linds0  48653  el0ldep  48654  lindsrng01  48656  snlindsntorlem  48658  ldepspr  48661  islindeps2  48671  zlmodzxzldep  48692  bigoval  48737  elbigo  48739  0aryfvalelfv  48823  1arympt1fv  48827  1arymaptfv  48828  1arymaptfo  48831  2arymptfv  48838  2arymaptfv  48839  2arymaptfo  48842  prelrrx2b  48902  rrx2plord  48908  rrx2vlinest  48929  rrx2linesl  48931  elrrx2linest2  48933  line2ylem  48939  line2xlem  48941  itsclc0  48959  itsclc0b  48960  itscnhlinecirc02p  48973  elfvne0  49036  iinfprg  49246  thincciso  49640  thinccisod  49641  setrecseq  49872  aacllem  49988