Theorem fveq1 6884

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 5104	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6522	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6546	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6546	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2820	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102  ℩cio 6492  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546

This theorem is used by:  fveq1i  6886  fveq1d  6887  iffv  6902  fvmptd3f  7009  fvmptdv2  7012  eqfnun  7036  fsnex  7291  f1prex  7292  isoeq1  7325  oveq  7426  elovmpt3imp  7678  ofrfvalg  7701  offval  7702  offval3  7994  bropopvvv  8101  bropfvvvvlem  8102  poseq  8175  soseq  8176  frrlem1  8304  frrlem13  8316  smoeq  8358  tfrlem12  8397  tz7.44-2  8415  tz7.44-3  8416  rdgeq1  8419  fsetfocdm  8883  fsetprcnex  8884  mapsncnv  8921  elixp2  8929  resixpfo  8964  elixpsn  8965  mapsnend  9064  enfixsn  9105  mapxpen  9162  ac6sfi  9275  ordtypelem7  9518  wemaplem1  9540  ixpiunwdom  9584  oemapval  9684  cantnf  9694  wemapwe  9698  cnfcom3clem  9706  ssttrcl  9716  ttrcltr  9717  ttrclss  9721  ttrclselem2  9727  updjud  10015  infxpenc2lem2  10099  fseqenlem1  10103  dfac8clem  10111  ac5num  10115  acni  10124  acni2  10125  acnlem  10127  dfac4  10201  dfac5lem5  10206  dfac2a  10208  dfac9  10215  dfacacn  10220  dfac12lem1  10222  dfac12r  10225  cofsmo  10347  cfsmolem  10348  cfsmo  10349  cfcoflem  10350  coftr  10351  alephsing  10354  isfin3ds  10407  fin23lem17  10416  fin23lem32  10422  fin23lem39  10428  isf33lem  10444  isf34lem6  10458  axcc2lem  10514  axcc3  10516  axdc2lem  10526  axdc3lem2  10529  axdc3lem3  10530  axdc3  10532  axdc4lem  10533  axcclem  10535  ac6num  10557  axdclem2  10598  konigthlem  10653  inar1  10860  1fv  13781  axdc4uzlem  14126  seqeq3  14149  seqof  14202  ccatfval  14718  wrdl1s1  14762  ccat1st1st  14776  cshf1  14961  cshweqrep  14972  wrdlen2i  15093  wwlktovf  15109  wwlktovf1  15110  wwlktovfo  15111  wrd2f1tovbij  15113  rtrclreclem1  15210  dfrtrclrec2  15211  rtrclreclem2  15212  rtrclreclem4  15214  dfrtrcl2  15215  clim  15661  rlim  15662  ello1  15682  elo1  15693  summo  15883  fsum  15886  prodmo  16103  fprod  16108  bpolylem  16214  bpolyval  16215  vdwlem6  17164  vdwlem8  17166  ramcl  17207  strfvnd  17363  prdsplusgval  17644  prdsmulrval  17646  prdsleval  17648  prdsdsval  17649  prdsvscaval  17650  xpsff1o  17739  isacs2  17827  isnat  18125  yonedalem3b  18453  yonedainv  18455  ischn  18781  chnind  18795  chnub  18796  ismgmhm  18885  ismhm  18980  prdspjmhm  19025  isgrpinv  19204  pwsmulg  19329  isghm  19430  cayleylem2  19627  symgfix2  19630  gsmsymgrfix  19642  gsmsymgreq  19646  symgfixelq  19647  pmtr3ncomlem2  19688  pmtrdifel  19694  pmtrdifwrdel  19699  pmtrdifwrdel2  19700  psgnunilem2  19709  psgnunilem3  19710  efgsdm  19944  efgredlemd  19958  efgredlem  19961  efgred  19962  efgrelexlema  19963  efgrelexlemb  19964  prdsgsum  20195  pwspjmhmmgpd  20557  pwsexpg  20558  pwsgprod  20559  isrnghm  20671  isrhm0  20706  isabv  21068  islmhm  21302  frgpcyg  21879  psgndiflemB  21906  psgndiflemA  21907  dsmmelbas  22045  frlmipval  22085  frlmphl  22087  uvcf1  22098  islindf  22118  islindf4  22144  psrmulfval  22251  evlslem2  22388  evlslem3  22389  evlslem1  22391  mpfrcl  22394  evlsvval  22399  evlsvvval  22402  selvval  22429  mplmapghm  22431  evlsvarval  22436  selvvvval  22451  psdval  22480  psdcoef  22481  psdadd  22484  psdmul  22487  psdmvr  22490  coe1fval  22523  coe1mul2lem2  22587  coe1tm  22592  madetsumid  22776  mvmulval  22858  marepvval0  22881  mulmarep1gsum2  22889  mdetleib2  22903  m1detdiag  22912  mdetralt  22923  mdetunilem7  22933  mdetunilem9  22935  m2detleiblem3  22944  m2detleiblem4  22945  m2detleib  22946  symgmatr01lem  22968  gsummatr01lem1  22970  gsummatr01lem4  22973  gsummatr01  22974  smadiadetlem3  22983  matunitlindflem2  22995  pmatcoe1fsupp  23019  pmatcollpw3lem  23101  pmatcollpw3fi1lem2  23105  iscnp  23555  1stcfb  23763  ptpjpre1  23890  elpt  23891  elptr  23892  ptpjopn  23931  dfac14  23937  upxp  23942  pthaus  23957  ptrescn  23958  xkoptsub  23973  cnmptkp  23999  xkofvcn  24003  cnmptk1p  24004  cnmptk2  24005  ptunhmeo  24127  ptcmplem3  24373  ptcmplem4  24374  symgtgp  24425  prdstmdd  24443  isucn  24596  imasdsf1olem  24692  prdsxmslem2  24848  tngngp3  24975  nmoval  25034  elcncf  25210  ishtpy  25293  pcoval  25332  om1elbas  25353  elpi1i  25367  iscau  25597  rrxds  25714  rrxdsfival  25734  ehl1eudisval  25742  ehl2eudisval  25744  mbfi1fseqlem6  26041  mbfi1flimlem  26043  isibl  26086  deg1ldg  26410  deg1leb  26413  elply2  26514  elplyr  26519  ne0p  26525  coeeu  26544  coelem  26545  coeeq  26546  coeidlem  26556  elqaalem3  26644  preimaaa  26646  qaa  26647  iaaOLD  26652  aareccl  26653  aannenlem2  26656  aaliou2  26667  dchrptlem2  27592  dchrpt  27594  dchrsum2  27595  sumdchr2  27597  dchrvmaeq0  27831  rpvmasum2  27839  dchrisum0re  27840  ostth  27966  ltsval  28004  nolesgn2o  28028  nogesgn1o  28030  noresle  28054  nosupprefixmo  28057  noinfprefixmo  28058  nosupcbv  28059  nosupfv  28063  noinfcbv  28074  noinffv  28078  iscgrg  28975  isismt  28997  israg  29172  elcgrabasi  29375  elcgrabasrd  29376  cgrabasimass  29378  iseqlg  29412  brbtwn  29477  brbtwn2  29483  colinearalg  29488  axsegconlem1  29495  axsegcon  29505  ax5seglem5  29511  axpasch  29519  axlowdim  29539  axeuclidlem  29540  axcontlem1  29542  axcontlem2  29543  axcontlem5  29546  vtxdgfval  30048  1egrvtxdg1  30090  isewlk  30183  iswlk  30191  uspgr2wlkeq2  30227  iswlkon  30236  isclwlk  30360  iscrct  30377  iscycl  30378  iswwlks  30425  wwlknon  30446  wlkiswwlks2  30464  wwlksnredwwlkn0  30485  wlksnwwlknvbij  30497  wwlksnextproplem3  30500  wwlksnextprop  30501  umgr2wlk  30538  midwwlks2s3  30541  elwwlks2  30558  elwspths2spth  30559  rusgrnumwwlkslem  30561  rusgrnumwwlkb0  30563  rusgrnumwwlks  30566  isclwwlk  30575  clwlkclwwlklem1  30590  clwwlkn1loopb  30634  clwwlkel  30637  clwwlkf  30638  clwwlkf1  30640  isclwwlknon  30682  clwwlknon1  30688  s2elclwwlknon2  30695  clwwlkvbij  30704  loop1cycl  30744  uhgr3cyclex  30783  fusgreg2wsplem  30934  fusgr2wsp2nb  30935  fusgreghash2wsp  30939  2clwwlkel  30950  extwwlkfabel  30954  numclwwlk1lem2fv  30957  numclwwlk1lem2  30961  clwwlknonclwlknonf1o  30963  dlwwlknondlwlknonf1o  30966  numclwwlk2lem1  30977  numclwlk2lem2f  30978  numclwlk2lem2f1o  30980  ex-fv  31044  isnvlem  31212  islno  31355  nmooval  31365  nmblolbi  31402  isphg  31419  ajmoi  31460  ajval  31463  ubthlem3  31474  htthlem  31519  hcau  31786  hlimi  31790  hosmval  32337  hommval  32338  hodmval  32339  hfsmval  32340  hfmmval  32341  adjmo  32434  nmopval  32458  elcnop  32459  ellnop  32460  elunop  32474  elhmop  32475  nmfnval  32478  elcnfn  32484  ellnfn  32485  adjeu  32491  adjval  32492  eigvecval  32498  eigvalfval  32499  adj1  32535  adjeq  32537  hmopadj2  32543  lnopeq0i  32609  lnopeq  32611  elunop2  32615  lnophm  32621  hmopco  32625  nmbdoplb  32627  nmcoplb  32632  lnopcon  32637  lnfn0  32649  lnfnmul  32650  nmbdfnlb  32652  nmcfnlb  32656  lnfncon  32658  riesz4  32666  riesz1  32667  cnlnadjlem9  32677  cnlnadjeu  32680  cnlnssadj  32682  nmopcoi  32697  bra11  32710  cnvbraval  32712  pjss2coi  32766  pjssdif2i  32776  pjssdif1i  32777  pjclem4  32801  pj3si  32809  pj3cor1i  32811  isst  32815  ishst  32816  stri  32859  hstri  32867  aciunf1lem  33256  ismnt  33544  mgcval  33548  fzo0pmtrlast  33653  elrgspnlem1  33803  elrgspnlem2  33804  elrgspnlem3  33805  elrgspnlem4  33806  elrgspn  33807  elrgspnsubrunlem1  33808  linds2eq  33936  elrspunidl  33978  elrspunsn  33979  dfufd2lem  34081  psrnzr  34144  0mplrim  34146  0mplric  34147  selvply1rhmlema  34150  selvply1rhmlemb  34151  selvply1rhmlem1  34152  selvply1rhmlem3  34154  selvply1rhmlem5  34156  selvply1rhm  34157  mplidom  34160  extvfv  34165  extvfvv  34166  extvfvcl  34168  evlvarval  34173  evlextv  34174  mplvrpmga  34177  splysubrg  34192  issply  34193  vietalem  34211  vieta  34212  lbsdiflsp0  34258  fedgmullem1  34261  fedgmullem2  34262  fedgmul  34263  fldextrspunlsplem  34305  fldextrspunlsp  34306  fldext2chn  34360  constrextdg2lem  34380  constrextdg2  34381  lmatval  34445  mdetpmtr1  34455  zarcmplem  34513  ismeas  34832  isrnmeas  34833  cntnevol  34861  carsgval  34935  sitgval  34964  eulerpartleme  34995  eulerpartlemd  34998  eulerpartlemr  35006  eulerpartlemgvv  35008  eulerpart  35014  cndprobval  35065  signstfvneq0  35201  reprsum  35242  reprsuc  35244  reprpmtf1o  35255  reprdifc  35256  breprexp  35262  vtsval  35266  hgt750lemb  35285  hgt750lema  35286  hgt750leme  35287  bnj66  35490  bnj106  35498  bnj125  35502  bnj154  35508  bnj155  35509  bnj526  35518  bnj540  35522  bnj609  35547  bnj611  35548  bnj893  35558  bnj1000  35571  bnj1014  35591  bnj1015  35592  bnj1234  35643  bnj1463  35685  fineqvnttrclse  35792  gblacfnacd  35881  derangenlem  35936  subfacp1lem3  35947  subfacp1lem5  35949  subfacp1lem6  35950  subfacp1  35951  sconnpht  35994  cnpconn  35995  txpconn  35997  ptpconn  35998  indispconn  35999  connpconn  36000  cvxpconn  36007  cvmliftmo  36049  cvmliftlem14  36062  cvmliftlem15  36063  cvmliftiota  36066  cvmlift2  36081  cvmliftphtlem  36082  cvmlift3lem2  36085  cvmlift3lem6  36089  cvmlift3lem7  36090  cvmlift3lem9  36092  cvmlift3  36093  satfv1lem  36127  satfv1  36128  sategoelfvb  36184  mrsubff1  36279  mrsub0  36281  mrsubccat  36283  mrsubcn  36284  elmsubrn  36293  msubrn  36294  msubco  36296  msubvrs  36325  mclsax  36334  shftvalg  36497  fwddifval  36927  fwddifnval  36928  bj-evalval  37996  unceq  38525  poimirlem17  38556  poimirlem20  38559  poimirlem22  38561  poimirlem23  38562  poimirlem27  38566  poimirlem28  38567  poimirlem30  38569  poimirlem31  38570  poimirlem32  38571  poimir  38572  broucube  38573  voliunnfl  38583  volsupnfl  38584  itg2addnclem  38590  itg2addnclem3  38592  itg2addnc  38593  ftc1anclem2  38613  ftc1anclem5  38616  upixp  38664  fdc  38680  isismty  38736  rrnmval  38763  elghomlem2OLD  38821  isrngohom  38900  islfl  40118  isopos  40238  islaut  41141  ispautN  41157  isldil  41168  isltrn  41177  ltrnid  41193  ltrneq2  41206  isdilN  41212  istrnN  41215  trlval  41220  ltrneq3  41266  cdleme50ex  41617  cdleme  41618  cdlemg1a  41628  ltrniotaval  41639  ltrniotavalbN  41642  cdlemeiota  41643  cdlemg2jlemOLDN  41651  cdlemg2fvlem  41652  cdlemg2klem  41653  istendo  41818  tendoplcbv  41833  tendopl  41834  tendoicbv  41851  tendoi  41852  tendoid0  41883  tendo1ne0  41886  cdlemksv2  41905  cdlemkuv2  41925  cdlemk33N  41967  cdlemk34  41968  cdlemk36  41971  cdlemk19u  42028  cdlemk  42032  tendoex  42033  dvavsca  42075  dvhvscacbv  42156  dvhvscaval  42157  dicopelval  42235  dicelval1sta  42245  diclspsn  42252  dihmeetlem13N  42377  dih1dimatlem0  42386  dih1dimatlem  42387  dihpN  42394  islpolN  42541  hdmap1fval  42854  hdmapfval  42885  sticksstones1  43197  sticksstones2  43198  sticksstones3  43199  sticksstones8  43204  sticksstones10  43206  sticksstones11  43207  sticksstones12a  43208  sticksstones12  43209  sticksstones15  43212  frlmsnic  43605  uvcn0  43607  evlsbagval  43615  evlselv  43618  fsuppssindlem2  43621  fsuppssind  43622  frlmnzcoordval  43654  sn-isghm  43685  ismrc  43712  mzpclval  43736  mzpsubst  43759  mzprename  43760  mzpcompact2lem  43762  eldioph  43769  eldioph2  43773  eldioph2b  43774  eldioph3  43777  rexrabdioph  43801  2rexfrabdioph  43803  3rexfrabdioph  43804  4rexfrabdioph  43805  6rexfrabdioph  43806  7rexfrabdioph  43807  eldioph4i  43819  rabren3dioph  43822  mzpcong  43979  jm2.27dlem1  44016  wepwsolem  44049  aomclem6  44061  aomclem8  44063  dfac11  44064  dgraalem  44147  dgraaub  44150  dgraa0p  44151  mpaaeu  44152  mpaalem  44154  aaitgo  44164  rngunsnply  44171  cantnfresb  44326  tfsconcatun  44339  nvocnvb  44423  eliunov2  44679  rfovcnvfvd  45007  fsovfvd  45010  fsovcnvlem  45013  dssmapfv2d  45018  dssmapnvod  45020  clsk1independent  45046  ntrclskb  45069  ntrclsk13  45071  gneispace2  45132  mnringmulrvald  45225  dvconstbi  45318  addrval  45448  subrval  45449  mulvval  45450  relpeq1  45934  fnchoice  46046  refsum2cnlem1  46054  choicefi  46214  axccdom  46235  fmulcl  46593  fmuldfeqlem1  46594  mccllem  46609  mccl  46610  climf  46634  climf2  46676  dvnprodlem1  46956  dvnprodlem3  46958  dvnprod  46959  stoweidlem2  47012  stoweidlem6  47016  stoweidlem8  47018  stoweidlem9  47019  stoweidlem15  47025  stoweidlem16  47026  stoweidlem17  47027  stoweidlem18  47028  stoweidlem21  47031  stoweidlem27  47037  stoweidlem31  47041  stoweidlem36  47046  stoweidlem37  47047  stoweidlem41  47051  stoweidlem43  47053  stoweidlem44  47054  stoweidlem45  47055  stoweidlem46  47056  stoweidlem48  47058  stoweidlem51  47061  stoweidlem55  47065  stoweidlem59  47069  stoweidlem60  47070  stoweidlem62  47072  fourierdlem2  47119  fourierdlem3  47120  elaa2lem  47243  etransclem11  47255  etransclem24  47268  etransclem26  47270  etransclem28  47272  etransclem35  47279  rrndistlt  47300  ioorrnopn  47315  subsaliuncllem  47367  sge0val  47376  ismea  47461  caragenval  47503  isome  47504  isomenndlem  47540  hoicvrrex  47566  ovnlecvr  47568  ovncvrrp  47574  ovn0lem  47575  ovnsubaddlem1  47580  ovnsubadd  47582  hsphoif  47586  hoidmvval  47587  hsphoival  47589  hoidmvlelem3  47607  hoidmvlelem5  47609  hoidmvle  47610  ovnhoilem1  47611  ovnhoi  47613  ovnlecvr2  47620  ovncvr2  47621  hoidifhspval2  47625  hoiqssbllem2  47633  hspmbllem2  47637  hspmbllem3  47638  hspmbl  47639  ovnovollem1  47666  smfmullem2  47802  smfmul  47805  smfpimcclem  47817  chnerlem1  47892  sqrtnnaa  47913  sqrtnzqaa  47914  sinnpoly  47941  cfsetsnfsetfv  48127  cfsetsnfsetfo  48130  iccpart  48498  iccpartiun  48516  icceuelpart  48518  nnsum3primes4  48886  nnsum3primesgbe  48890  nnsum4primesodd  48894  nnsum4primesoddALTV  48895  nnsum4primeseven  48898  nnsum4primesevenALTV  48899  bgoldbtbnd  48907  isisubgr  48960  isgrim  48980  grimidvtxedg  48983  grimcnv  48986  grimco  48987  isuspgrim0  48992  gricushgr  49015  ushggricedg  49025  uhgrimisgrgric  49029  isgrtri  49041  isubgr3stgrlem3  49066  isubgr3stgr  49073  isgrlim  49080  uspgrlim  49090  grlicref  49110  grlicsym  49111  grlictr  49113  grlimedgnedg  49229  isupwlk  49234  lincval  49521  lincdifsn  49536  linindslinci  49560  lindslinindsimp1  49569  linds0  49577  el0ldep  49578  lindsrng01  49580  snlindsntorlem  49582  ldepspr  49585  islindeps2  49595  zlmodzxzldep  49616  bigoval  49661  elbigo  49663  0aryfvalelfv  49747  1arympt1fv  49751  1arymaptfv  49752  1arymaptfo  49755  2arymptfv  49762  2arymaptfv  49763  2arymaptfo  49766  prelrrx2b  49826  rrx2plord  49832  rrx2vlinest  49853  rrx2linesl  49855  elrrx2linest2  49857  line2ylem  49863  line2xlem  49865  itsclc0  49883  itsclc0b  49884  itscnhlinecirc02p  49897  elfvne0  49959  iinfprg  50167  thincciso  50561  thinccisod  50562  setrecseq  50788  aacllem  50939  crosspval  50954  crosspdot0lem  50963  veronesevald  50971