Theorem fveq1 6826

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 5074	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6469	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6493	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6493	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2799	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1547   class class class wbr 5072  ℩cio 6439  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-ss 3900  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493

This theorem is referenced by:  fveq1i  6828  fveq1d  6829  iffv  6844  fvmptd3f  6951  fvmptdv2  6954  eqfnun  6978  fsnex  7227  f1prex  7228  isoeq1  7261  oveq  7362  elovmpt3imp  7613  ofrfvalg  7628  offval  7629  offval3  7924  bropopvvv  8029  bropfvvvvlem  8030  poseq  8098  soseq  8099  frrlem1  8226  frrlem13  8238  smoeq  8280  tfrlem12  8318  tz7.44-2  8336  tz7.44-3  8337  rdgeq1  8340  fsetfocdm  8798  fsetprcnex  8799  mapsncnv  8831  elixp2  8839  resixpfo  8874  elixpsn  8875  mapsnend  8973  enfixsn  9014  mapxpen  9071  ac6sfi  9184  ordtypelem7  9429  wemaplem1  9451  ixpiunwdom  9495  oemapval  9595  cantnf  9605  wemapwe  9609  cnfcom3clem  9617  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  updjud  9849  infxpenc2lem2  9933  fseqenlem1  9937  dfac8clem  9945  ac5num  9949  acni  9958  acni2  9959  acnlem  9961  dfac4  10035  dfac5lem5  10040  dfac2a  10043  dfac9  10050  dfacacn  10055  dfac12lem1  10057  dfac12r  10060  cofsmo  10182  cfsmolem  10183  cfsmo  10184  cfcoflem  10185  coftr  10186  alephsing  10189  isfin3ds  10242  fin23lem17  10251  fin23lem32  10257  fin23lem39  10263  isf33lem  10279  isf34lem6  10293  axcc2lem  10349  axcc3  10351  axdc2lem  10361  axdc3lem2  10364  axdc3lem3  10365  axdc3  10367  axdc4lem  10368  axcclem  10370  ac6num  10392  axdclem2  10433  konigthlem  10482  inar1  10689  1fv  13592  axdc4uzlem  13936  seqeq3  13959  seqof  14012  ccatfval  14526  wrdl1s1  14568  ccat1st1st  14582  cshf1  14763  cshweqrep  14774  wrdlen2i  14895  wwlktovf  14909  wwlktovf1  14910  wwlktovfo  14911  wrd2f1tovbij  14913  rtrclreclem1  15010  dfrtrclrec2  15011  rtrclreclem2  15012  rtrclreclem4  15014  dfrtrcl2  15015  clim  15447  rlim  15448  ello1  15468  elo1  15479  summo  15670  fsum  15673  prodmo  15892  fprod  15897  bpolylem  16004  bpolyval  16005  vdwlem6  16948  vdwlem8  16950  ramcl  16991  strfvnd  17146  prdsplusgval  17427  prdsmulrval  17429  prdsleval  17431  prdsdsval  17432  prdsvscaval  17433  xpsff1o  17522  isacs2  17610  isnat  17908  yonedalem3b  18236  yonedainv  18238  ischn  18564  chnind  18578  chnub  18579  ismgmhm  18655  ismhm  18744  prdspjmhm  18788  isgrpinv  18960  pwsmulg  19086  isghm  19181  isghmOLD  19182  cayleylem2  19379  symgfix2  19382  gsmsymgrfix  19394  gsmsymgreq  19398  symgfixelq  19399  pmtr3ncomlem2  19440  pmtrdifel  19446  pmtrdifwrdel  19451  pmtrdifwrdel2  19452  psgnunilem2  19461  psgnunilem3  19462  efgsdm  19696  efgredlemd  19710  efgredlem  19713  efgred  19714  efgrelexlema  19715  efgrelexlemb  19716  prdsgsum  19947  pwspjmhmmgpd  20298  pwsexpg  20299  pwsgprod  20300  isrnghm  20412  isabv  20783  islmhm  21017  frgpcyg  21548  psgndiflemB  21575  psgndiflemA  21576  dsmmelbas  21714  frlmipval  21754  frlmphl  21756  uvcf1  21767  islindf  21787  islindf4  21813  psrmulfval  21918  evlslem2  22055  evlslem3  22056  evlslem1  22058  mpfrcl  22061  evlsvval  22066  evlsvvval  22069  selvval  22096  mplmapghm  22098  evlsvarval  22103  selvvvval  22118  psdval  22147  psdcoef  22148  psdadd  22151  psdmul  22154  psdmvr  22157  coe1fval  22190  coe1mul2lem2  22254  coe1tm  22259  madetsumid  22444  mvmulval  22526  marepvval0  22549  mulmarep1gsum2  22557  mdetleib2  22571  m1detdiag  22580  mdetralt  22591  mdetunilem7  22601  mdetunilem9  22603  m2detleiblem3  22612  m2detleiblem4  22613  m2detleib  22614  symgmatr01lem  22636  gsummatr01lem1  22638  gsummatr01lem4  22641  gsummatr01  22642  smadiadetlem3  22651  pmatcoe1fsupp  22684  pmatcollpw3lem  22766  pmatcollpw3fi1lem2  22770  iscnp  23220  1stcfb  23428  ptpjpre1  23554  elpt  23555  elptr  23556  ptpjopn  23595  dfac14  23601  upxp  23606  pthaus  23621  ptrescn  23622  xkoptsub  23637  cnmptkp  23663  xkofvcn  23667  cnmptk1p  23668  cnmptk2  23669  ptunhmeo  23791  ptcmplem3  24037  ptcmplem4  24038  symgtgp  24089  prdstmdd  24107  isucn  24260  imasdsf1olem  24356  prdsxmslem2  24512  tngngp3  24639  nmoval  24698  elcncf  24874  ishtpy  24957  pcoval  24996  om1elbas  25017  elpi1i  25031  iscau  25261  rrxds  25378  rrxdsfival  25398  ehl1eudisval  25406  ehl2eudisval  25408  mbfi1fseqlem6  25705  mbfi1flimlem  25707  isibl  25750  deg1ldg  26075  deg1leb  26078  elply2  26179  elplyr  26184  ne0p  26190  coeeu  26208  coelem  26209  coeeq  26210  coeidlem  26220  elqaalem3  26305  qaa  26307  iaa  26309  aareccl  26310  aannenlem2  26313  aaliou2  26324  dchrptlem2  27246  dchrpt  27248  dchrsum2  27249  sumdchr2  27251  dchrvmaeq0  27485  rpvmasum2  27493  dchrisum0re  27494  ostth  27620  ltsval  27629  nolesgn2o  27653  nogesgn1o  27655  noresle  27679  nosupprefixmo  27682  noinfprefixmo  27683  nosupcbv  27684  nosupfv  27688  noinfcbv  27699  noinffv  27703  iscgrg  28598  isismt  28620  israg  28783  iseqlg  28953  brbtwn  28986  brbtwn2  28992  colinearalg  28997  axsegconlem1  29004  axsegcon  29014  ax5seglem5  29020  axpasch  29028  axlowdim  29048  axeuclidlem  29049  axcontlem1  29051  axcontlem2  29052  axcontlem5  29055  vtxdgfval  29554  1egrvtxdg1  29596  isewlk  29689  iswlk  29697  uspgr2wlkeq2  29733  iswlkon  29742  isclwlk  29859  iscrct  29876  iscycl  29877  iswwlks  29922  wwlknon  29943  wlkiswwlks2  29961  wwlksnredwwlkn0  29982  wlksnwwlknvbij  29994  wwlksnextproplem3  29997  wwlksnextprop  29998  umgr2wlk  30035  midwwlks2s3  30038  elwwlks2  30055  elwspths2spth  30056  rusgrnumwwlkslem  30058  rusgrnumwwlkb0  30060  rusgrnumwwlks  30063  isclwwlk  30072  clwlkclwwlklem1  30087  clwwlkn1loopb  30131  clwwlkel  30134  clwwlkf  30135  clwwlkf1  30137  isclwwlknon  30179  clwwlknon1  30185  s2elclwwlknon2  30192  clwwlkvbij  30201  uhgr3cyclex  30270  fusgreg2wsplem  30421  fusgr2wsp2nb  30422  fusgreghash2wsp  30426  2clwwlkel  30437  extwwlkfabel  30441  numclwwlk1lem2fv  30444  numclwwlk1lem2  30448  clwwlknonclwlknonf1o  30450  dlwwlknondlwlknonf1o  30453  numclwwlk2lem1  30464  numclwlk2lem2f  30465  numclwlk2lem2f1o  30467  ex-fv  30531  isnvlem  30699  islno  30842  nmooval  30852  nmblolbi  30889  isphg  30906  ajmoi  30947  ajval  30950  ubthlem3  30961  htthlem  31006  hcau  31273  hlimi  31277  hosmval  31824  hommval  31825  hodmval  31826  hfsmval  31827  hfmmval  31828  adjmo  31921  nmopval  31945  elcnop  31946  ellnop  31947  elunop  31961  elhmop  31962  nmfnval  31965  elcnfn  31971  ellnfn  31972  adjeu  31978  adjval  31979  eigvecval  31985  eigvalfval  31986  adj1  32022  adjeq  32024  hmopadj2  32030  lnopeq0i  32096  lnopeq  32098  elunop2  32102  lnophm  32108  hmopco  32112  nmbdoplb  32114  nmcoplb  32119  lnopcon  32124  lnfn0  32136  lnfnmul  32137  nmbdfnlb  32139  nmcfnlb  32143  lnfncon  32145  riesz4  32153  riesz1  32154  cnlnadjlem9  32164  cnlnadjeu  32167  cnlnssadj  32169  nmopcoi  32184  bra11  32197  cnvbraval  32199  pjss2coi  32253  pjssdif2i  32263  pjssdif1i  32264  pjclem4  32288  pj3si  32296  pj3cor1i  32298  isst  32302  ishst  32303  stri  32346  hstri  32354  aciunf1lem  32754  ismnt  33062  mgcval  33066  fzo0pmtrlast  33173  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnlem3  33325  elrgspnlem4  33326  elrgspn  33327  elrgspnsubrunlem1  33328  linds2eq  33464  elrspunidl  33511  elrspunsn  33512  dfufd2lem  33632  psrnzr  33696  0mplrim  33698  0mplric  33699  selvply1rhmlema  33702  selvply1rhmlemb  33703  selvply1rhmlem1  33704  selvply1rhmlem3  33706  selvply1rhmlem5  33708  selvply1rhm  33709  mplidom  33712  extvfv  33717  extvfvv  33718  extvfvcl  33720  evlvarval  33725  evlextv  33726  mplvrpmga  33729  splysubrg  33744  issply  33745  vietalem  33763  vieta  33764  lbsdiflsp0  33810  fedgmullem1  33813  fedgmullem2  33814  fedgmul  33815  fldextrspunlsplem  33857  fldextrspunlsp  33858  fldext2chn  33912  constrextdg2lem  33932  constrextdg2  33933  lmatval  33997  mdetpmtr1  34007  zarcmplem  34065  ismeas  34383  isrnmeas  34384  cntnevol  34412  carsgval  34487  sitgval  34516  eulerpartleme  34547  eulerpartlemd  34550  eulerpartlemr  34558  eulerpartlemgvv  34560  eulerpart  34566  cndprobval  34617  signstfvneq0  34756  reprsum  34797  reprsuc  34799  reprpmtf1o  34810  reprdifc  34811  breprexp  34817  vtsval  34821  hgt750lemb  34840  hgt750lema  34841  hgt750leme  34842  bnj66  35042  bnj106  35050  bnj125  35054  bnj154  35060  bnj155  35061  bnj526  35070  bnj540  35074  bnj609  35099  bnj611  35100  bnj893  35110  bnj1000  35123  bnj1014  35143  bnj1015  35144  bnj1234  35195  bnj1463  35237  fineqvnttrclse  35305  gblacfnacd  35330  loop1cycl  35365  derangenlem  35399  subfacp1lem3  35410  subfacp1lem5  35412  subfacp1lem6  35413  subfacp1  35414  sconnpht  35457  cnpconn  35458  txpconn  35460  ptpconn  35461  indispconn  35462  connpconn  35463  cvxpconn  35470  cvmliftmo  35512  cvmliftlem14  35525  cvmliftlem15  35526  cvmliftiota  35529  cvmlift2  35544  cvmliftphtlem  35545  cvmlift3lem2  35548  cvmlift3lem6  35552  cvmlift3lem7  35553  cvmlift3lem9  35555  cvmlift3  35556  satfv1lem  35590  satfv1  35591  sategoelfvb  35647  mrsubff1  35742  mrsub0  35744  mrsubccat  35746  mrsubcn  35747  elmsubrn  35756  msubrn  35757  msubco  35759  msubvrs  35788  mclsax  35797  shftvalg  35960  fwddifval  36390  fwddifnval  36391  bj-evalval  37433  unceq  37964  matunitlindflem2  37984  poimirlem17  38004  poimirlem20  38007  poimirlem22  38009  poimirlem23  38010  poimirlem27  38014  poimirlem28  38015  poimirlem30  38017  poimirlem31  38018  poimirlem32  38019  poimir  38020  broucube  38021  voliunnfl  38031  volsupnfl  38032  itg2addnclem  38038  itg2addnclem3  38040  itg2addnc  38041  ftc1anclem2  38061  ftc1anclem5  38064  upixp  38096  fdc  38112  isismty  38168  rrnmval  38195  elghomlem2OLD  38253  isrngohom  38332  islfl  39552  isopos  39672  islaut  40575  ispautN  40591  isldil  40602  isltrn  40611  ltrnid  40627  ltrneq2  40640  isdilN  40646  istrnN  40649  trlval  40654  ltrneq3  40700  cdleme50ex  41051  cdleme  41052  cdlemg1a  41062  ltrniotaval  41073  ltrniotavalbN  41076  cdlemeiota  41077  cdlemg2jlemOLDN  41085  cdlemg2fvlem  41086  cdlemg2klem  41087  istendo  41252  tendoplcbv  41267  tendopl  41268  tendoicbv  41285  tendoi  41286  tendoid0  41317  tendo1ne0  41320  cdlemksv2  41339  cdlemkuv2  41359  cdlemk33N  41401  cdlemk34  41402  cdlemk36  41405  cdlemk19u  41462  cdlemk  41466  tendoex  41467  dvavsca  41509  dvhvscacbv  41590  dvhvscaval  41591  dicopelval  41669  dicelval1sta  41679  diclspsn  41686  dihmeetlem13N  41811  dih1dimatlem0  41820  dih1dimatlem  41821  dihpN  41828  islpolN  41975  hdmap1fval  42288  hdmapfval  42319  sticksstones1  42631  sticksstones2  42632  sticksstones3  42633  sticksstones8  42638  sticksstones10  42640  sticksstones11  42641  sticksstones12a  42642  sticksstones12  42643  sticksstones15  42646  frlmsnic  43026  uvcn0  43028  evlsbagval  43036  evlselv  43039  fsuppssindlem2  43042  fsuppssind  43043  prjspnfv01  43074  prjspner01  43075  prjspner1  43076  sn-isghm  43123  ismrc  43150  mzpclval  43174  mzpsubst  43197  mzprename  43198  mzpcompact2lem  43200  eldioph  43207  eldioph2  43211  eldioph2b  43212  eldioph3  43215  rexrabdioph  43239  2rexfrabdioph  43241  3rexfrabdioph  43242  4rexfrabdioph  43243  6rexfrabdioph  43244  7rexfrabdioph  43245  eldioph4i  43257  rabren3dioph  43260  mzpcong  43417  jm2.27dlem1  43454  wepwsolem  43487  aomclem6  43504  aomclem8  43506  dfac11  43507  dgraalem  43590  dgraaub  43593  dgraa0p  43594  mpaaeu  43595  mpaalem  43597  aaitgo  43607  rngunsnply  43614  cantnfresb  43769  tfsconcatun  43782  nvocnvb  43866  eliunov2  44123  rfovcnvfvd  44451  fsovfvd  44454  fsovcnvlem  44457  dssmapfv2d  44462  dssmapnvod  44464  clsk1independent  44490  ntrclskb  44513  ntrclsk13  44515  gneispace2  44576  mnringmulrvald  44671  dvconstbi  44778  addrval  44909  subrval  44910  mulvval  44911  relpeq1  45388  fnchoice  45477  refsum2cnlem1  45485  choicefi  45646  axccdom  45667  fmulcl  46026  fmuldfeqlem1  46027  mccllem  46042  mccl  46043  climf  46067  climf2  46109  dvnprodlem1  46389  dvnprodlem3  46391  dvnprod  46392  stoweidlem2  46445  stoweidlem6  46449  stoweidlem8  46451  stoweidlem9  46452  stoweidlem15  46458  stoweidlem16  46459  stoweidlem17  46460  stoweidlem18  46461  stoweidlem21  46464  stoweidlem27  46470  stoweidlem31  46474  stoweidlem36  46479  stoweidlem37  46480  stoweidlem41  46484  stoweidlem43  46486  stoweidlem44  46487  stoweidlem45  46488  stoweidlem46  46489  stoweidlem48  46491  stoweidlem51  46494  stoweidlem55  46498  stoweidlem59  46502  stoweidlem60  46503  stoweidlem62  46505  fourierdlem2  46552  fourierdlem3  46553  elaa2lem  46676  etransclem11  46688  etransclem24  46701  etransclem26  46703  etransclem28  46705  etransclem35  46712  rrndistlt  46733  ioorrnopn  46748  subsaliuncllem  46800  sge0val  46809  ismea  46894  caragenval  46936  isome  46937  isomenndlem  46973  hoicvrrex  46999  ovnlecvr  47001  ovncvrrp  47007  ovn0lem  47008  ovnsubaddlem1  47013  ovnsubadd  47015  hsphoif  47019  hoidmvval  47020  hsphoival  47022  hoidmvlelem3  47040  hoidmvlelem5  47042  hoidmvle  47043  ovnhoilem1  47044  ovnhoi  47046  ovnlecvr2  47053  ovncvr2  47054  hoidifhspval2  47058  hoiqssbllem2  47066  hspmbllem2  47070  hspmbllem3  47071  hspmbl  47072  ovnovollem1  47099  smfmullem2  47235  smfmul  47238  smfpimcclem  47250  chnerlem1  47327  nthrucw  47331  sinnpoly  47354  cfsetsnfsetfv  47520  cfsetsnfsetfo  47523  iccpart  47891  iccpartiun  47909  icceuelpart  47911  nnsum3primes4  48279  nnsum3primesgbe  48283  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  bgoldbtbnd  48300  isisubgr  48353  isgrim  48373  grimidvtxedg  48376  grimcnv  48379  grimco  48380  isuspgrim0  48385  gricushgr  48408  ushggricedg  48418  uhgrimisgrgric  48422  isgrtri  48434  isubgr3stgrlem3  48459  isubgr3stgr  48466  isgrlim  48473  uspgrlim  48483  grlicref  48503  grlicsym  48504  grlictr  48506  grlimedgnedg  48622  isupwlk  48627  lincval  48900  lincdifsn  48915  linindslinci  48939  lindslinindsimp1  48948  linds0  48956  el0ldep  48957  lindsrng01  48959  snlindsntorlem  48961  ldepspr  48964  islindeps2  48974  zlmodzxzldep  48995  bigoval  49040  elbigo  49042  0aryfvalelfv  49126  1arympt1fv  49130  1arymaptfv  49131  1arymaptfo  49134  2arymptfv  49141  2arymaptfv  49142  2arymaptfo  49145  prelrrx2b  49205  rrx2plord  49211  rrx2vlinest  49232  rrx2linesl  49234  elrrx2linest2  49236  line2ylem  49242  line2xlem  49244  itsclc0  49262  itsclc0b  49263  itscnhlinecirc02p  49276  elfvne0  49339  iinfprg  49549  thincciso  49943  thinccisod  49944  setrecseq  50175  aacllem  50291