Theorem fveq1 6492

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 4925	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6167	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6190	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6190	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2833	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1507   class class class wbr 4923  ℩cio 6144  ‘cfv 6182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-rex 3088  df-uni 4707  df-br 4924  df-iota 6146  df-fv 6190

This theorem is referenced by:  fveq1i  6494  fveq1d  6495  iffv  6510  fvmptd3f  6603  fvmptdv2  6606  fsnex  6858  f1prex  6859  isoeq1  6887  oveq  6976  elovmpt3imp  7214  offval  7228  ofrfval  7229  offval3  7488  bropopvvv  7586  bropfvvvvlem  7587  wfrlem1  7750  wfrlem3a  7753  wfrlem15  7766  smoeq  7784  tfrlem12  7822  tz7.44-2  7840  tz7.44-3  7841  rdgeq1  7844  mapsncnv  8247  elixp2  8255  resixpfo  8289  elixpsn  8290  mapsnend  8377  enfixsn  8414  mapxpen  8471  ac6sfi  8549  ordtypelem7  8775  wemaplem1  8797  ixpiunwdom  8842  oemapval  8932  cantnf  8942  wemapwe  8946  cnfcom3clem  8954  updjud  9149  infxpenc2lem2  9232  fseqenlem1  9236  dfac8clem  9244  ac5num  9248  acni  9257  acni2  9258  acnlem  9260  dfac4  9334  dfac5lem5  9339  dfac2a  9341  dfac9  9348  dfacacn  9353  dfac12lem1  9355  dfac12r  9358  cofsmo  9481  cfsmolem  9482  cfsmo  9483  cfcoflem  9484  coftr  9485  alephsing  9488  isfin3ds  9541  fin23lem17  9550  fin23lem32  9556  fin23lem39  9562  isf33lem  9578  isf34lem6  9592  axcc2lem  9648  axcc3  9650  axdc2lem  9660  axdc3lem2  9663  axdc3lem3  9664  axdc3  9666  axdc4lem  9667  axcclem  9669  ac6num  9691  axdclem2  9732  konigthlem  9780  inar1  9987  1fv  12835  axdc4uzlem  13159  seqeq3  13182  seqof  13235  ccatfval  13726  wrdl1s1  13767  ccat1st1st  13781  cshf1  14024  cshweqrep  14035  wrdlen2i  14156  wwlktovf  14171  wwlktovf1  14172  wwlktovfo  14173  wrd2f1tovbij  14175  dfrtrclrec2  14267  rtrclreclem1  14268  rtrclreclem2  14269  rtrclreclem4  14271  dfrtrcl2  14272  clim  14702  rlim  14703  ello1  14723  elo1  14734  summo  14924  fsum  14927  prodmo  15140  fprod  15145  bpolylem  15252  bpolyval  15253  vdwlem6  16168  vdwlem8  16170  ramcl  16211  strfvnd  16348  prdsplusgval  16592  prdsmulrval  16594  prdsleval  16596  prdsdsval  16597  prdsvscaval  16598  xpsff1o  16687  isacs2  16772  isnat  17065  yonedalem3b  17377  yonedainv  17379  ismhm  17795  prdspjmhm  17825  isgrpinv  17933  pwsmulg  18046  isghm  18119  cayleylem2  18292  symgfix2  18295  gsmsymgrfix  18307  gsmsymgreq  18311  symgfixelq  18312  pmtr3ncomlem2  18353  pmtrdifel  18359  pmtrdifwrdel  18364  pmtrdifwrdel2  18365  psgnunilem2  18375  psgnunilem3  18376  efgsdm  18604  efgredlemd  18619  efgredlem  18622  efgredlemOLD  18623  efgred  18624  efgrelexlema  18625  efgrelexlemb  18626  prdsgsum  18841  isabv  19302  islmhm  19511  psrmulfval  19869  evlslem2  19995  evlslem3  19997  evlslem1  19998  mpfrcl  20001  coe1fval  20066  coe1mul2lem2  20129  coe1tm  20134  frgpcyg  20412  psgndiflemB  20436  psgndiflemA  20437  dsmmelbas  20575  frlmipval  20615  frlmphl  20617  uvcf1  20628  islindf  20648  islindf4  20674  madetsumid  20764  mvmulval  20846  marepvval0  20869  mulmarep1gsum2  20877  mdetleib2  20891  m1detdiag  20900  mdetralt  20911  mdetunilem7  20921  mdetunilem9  20923  m2detleiblem3  20932  m2detleiblem4  20933  m2detleib  20934  symgmatr01lem  20956  gsummatr01lem1  20958  gsummatr01lem4  20961  gsummatr01  20962  smadiadetlem3  20971  pmatcoe1fsupp  21003  pmatcollpw3lem  21085  pmatcollpw3fi1lem2  21089  iscnp  21539  1stcfb  21747  ptpjpre1  21873  elpt  21874  elptr  21875  ptpjopn  21914  dfac14  21920  upxp  21925  pthaus  21940  ptrescn  21941  xkoptsub  21956  cnmptkp  21982  xkofvcn  21986  cnmptk1p  21987  cnmptk2  21988  ptunhmeo  22110  ptcmplem3  22356  ptcmplem4  22357  symgtgp  22403  prdstmdd  22425  isucn  22580  imasdsf1olem  22676  prdsxmslem2  22832  tngngp3  22958  nmoval  23017  elcncf  23190  ishtpy  23269  pcoval  23308  om1elbas  23329  elpi1i  23343  iscau  23572  rrxds  23689  rrxdsfival  23709  ehl1eudisval  23717  ehl2eudisval  23719  mbfi1fseqlem6  24014  mbfi1flimlem  24016  isibl  24059  deg1ldg  24379  deg1leb  24382  elply2  24479  elplyr  24484  ne0p  24490  coeeu  24508  coelem  24509  coeeq  24510  coeidlem  24520  elqaalem3  24603  qaa  24605  iaa  24607  aareccl  24608  aannenlem2  24611  aaliou2  24622  dchrptlem2  25533  dchrpt  25535  dchrsum2  25536  sumdchr2  25538  dchrvmaeq0  25772  rpvmasum2  25780  dchrisum0re  25781  ostth  25907  iscgrg  25990  isismt  26012  israg  26175  iseqlg  26346  brbtwn  26378  brbtwn2  26384  colinearalg  26389  axsegconlem1  26396  axsegcon  26406  ax5seglem5  26412  axpasch  26420  axlowdim  26440  axeuclidlem  26441  axcontlem1  26443  axcontlem2  26444  axcontlem5  26447  vtxdgfval  26942  1egrvtxdg1  26984  isewlk  27077  iswlk  27085  uspgr2wlkeq2  27121  iswlkon  27131  isclwlk  27252  iscrct  27269  iscycl  27270  iswwlks  27312  wwlknon  27333  wlkiswwlks2  27351  wwlksnredwwlkn0  27376  wwlksnredwwlkn0OLD  27377  wlksnwwlknvbij  27398  wwlksnextproplem3  27403  wwlksnextproplem3OLD  27404  wwlksnextprop  27405  wwlksnextpropOLD  27406  umgr2wlk  27445  midwwlks2s3  27448  elwwlks2  27462  elwspths2spth  27463  rusgrnumwwlkslem  27465  rusgrnumwwlkb0  27467  rusgrnumwwlks  27470  rusgrnumwwlksOLD  27471  isclwwlk  27480  clwlkclwwlklem1  27495  clwwlkn1loopb  27549  clwwlkel  27553  clwwlkfOLD  27554  clwwlkf1OLD  27556  clwwlkf  27559  clwwlkf1  27561  isclwwlknon  27609  clwwlknon1  27615  s2elclwwlknon2  27622  clwwlkvbij  27631  clwwlkvbijOLD  27632  uhgr3cyclex  27701  fusgreg2wsplem  27857  fusgr2wsp2nb  27858  fusgreghash2wsp  27862  2clwwlkel  27876  extwwlkfabel  27883  extwwlkfabelOLD  27884  numclwwlk1lem2fv  27888  numclwwlk1lem2fvOLD  27893  numclwwlk1lem2  27897  numclwwlk1lem2OLD  27898  clwwlknonclwlknonf1o  27900  clwwlknonclwlknonf1oOLD  27901  dlwwlknondlwlknonf1o  27906  dlwwlknondlwlknonf1oOLD  27907  numclwwlk2lem1  27919  numclwlk2lem2f  27920  numclwlk2lem2f1o  27922  numclwlk2lem2fOLD  27923  numclwlk2lem2f1oOLD  27925  ex-fv  27990  isnvlem  28154  islno  28297  nmooval  28307  nmblolbi  28344  isphg  28361  ajmoi  28403  ajval  28406  ubthlem3  28417  htthlem  28463  hcau  28730  hlimi  28734  hosmval  29283  hommval  29284  hodmval  29285  hfsmval  29286  hfmmval  29287  adjmo  29380  nmopval  29404  elcnop  29405  ellnop  29406  elunop  29420  elhmop  29421  nmfnval  29424  elcnfn  29430  ellnfn  29431  adjeu  29437  adjval  29438  eigvecval  29444  eigvalfval  29445  adj1  29481  adjeq  29483  hmopadj2  29489  lnopeq0i  29555  lnopeq  29557  elunop2  29561  lnophm  29567  hmopco  29571  nmbdoplb  29573  nmcoplb  29578  lnopcon  29583  lnfn0  29595  lnfnmul  29596  nmbdfnlb  29598  nmcfnlb  29602  lnfncon  29604  riesz4  29612  riesz1  29613  cnlnadjlem9  29623  cnlnadjeu  29626  cnlnssadj  29628  nmopcoi  29643  bra11  29656  cnvbraval  29658  pjss2coi  29712  pjssdif2i  29722  pjssdif1i  29723  pjclem4  29747  pj3si  29755  pj3cor1i  29757  isst  29761  ishst  29762  stri  29805  hstri  29813  aciunf1lem  30159  linds2eq  30568  lbsdiflsp0  30607  fedgmullem1  30610  fedgmullem2  30611  fedgmul  30612  lmatval  30677  mdetpmtr1  30687  ismeas  31060  isrnmeas  31061  cntnevol  31089  carsgval  31163  sitgval  31192  eulerpartleme  31223  eulerpartlemd  31226  eulerpartlemr  31234  eulerpartlemgvv  31236  eulerpart  31242  cndprobval  31294  signstfvneq0  31450  reprsum  31493  reprsuc  31495  reprpmtf1o  31506  reprdifc  31507  breprexp  31513  vtsval  31517  hgt750lemb  31536  hgt750lema  31537  hgt750leme  31538  bnj66  31740  bnj106  31748  bnj125  31752  bnj154  31758  bnj155  31759  bnj526  31768  bnj540  31772  bnj609  31797  bnj611  31798  bnj893  31808  bnj1000  31821  bnj1014  31840  bnj1015  31841  bnj1234  31891  bnj1463  31933  derangenlem  31963  subfacp1lem3  31974  subfacp1lem5  31976  subfacp1lem6  31977  subfacp1  31978  sconnpht  32021  cnpconn  32022  txpconn  32024  ptpconn  32025  indispconn  32026  connpconn  32027  cvxpconn  32034  cvmliftmo  32076  cvmliftlem14  32089  cvmliftlem15  32090  cvmliftiota  32093  cvmlift2  32108  cvmliftphtlem  32109  cvmlift3lem2  32112  cvmlift3lem6  32116  cvmlift3lem7  32117  cvmlift3lem9  32119  cvmlift3  32120  mrsubff1  32221  mrsub0  32223  mrsubccat  32225  mrsubcn  32226  elmsubrn  32235  msubrn  32236  msubco  32238  msubvrs  32267  mclsax  32276  shftvalg  32423  poseq  32556  soseq  32557  frrlem1  32584  frrlem13  32596  sltval  32615  nolesgn2o  32639  noresle  32661  noprefixmo  32663  nosupfv  32667  fwddifval  33084  fwddifnval  33085  bj-evalval  33810  unceq  34258  matunitlindflem2  34278  poimirlem17  34298  poimirlem20  34301  poimirlem22  34303  poimirlem23  34304  poimirlem27  34308  poimirlem28  34309  poimirlem30  34311  poimirlem31  34312  poimirlem32  34313  poimir  34314  broucube  34315  voliunnfl  34325  volsupnfl  34326  itg2addnclem  34332  itg2addnclem3  34334  itg2addnc  34335  ftc1anclem2  34357  ftc1anclem5  34360  eqfnun  34387  upixp  34394  fdc  34410  isismty  34469  rrnmval  34496  elghomlem2OLD  34554  isrngohom  34633  islfl  35589  isopos  35709  islaut  36612  ispautN  36628  isldil  36639  isltrn  36648  ltrnid  36664  ltrneq2  36677  isdilN  36683  istrnN  36686  trlval  36691  ltrneq3  36737  cdleme50ex  37088  cdleme  37089  cdlemg1a  37099  ltrniotaval  37110  ltrniotavalbN  37113  cdlemeiota  37114  cdlemg2jlemOLDN  37122  cdlemg2fvlem  37123  cdlemg2klem  37124  istendo  37289  tendoplcbv  37304  tendopl  37305  tendoicbv  37322  tendoi  37323  tendoid0  37354  tendo1ne0  37357  cdlemksv2  37376  cdlemkuv2  37396  cdlemk33N  37438  cdlemk34  37439  cdlemk36  37442  cdlemk19u  37499  cdlemk  37503  tendoex  37504  dvavsca  37546  dvhvscacbv  37627  dvhvscaval  37628  dicopelval  37706  dicelval1sta  37716  diclspsn  37723  dihmeetlem13N  37848  dih1dimatlem0  37857  dih1dimatlem  37858  dihpN  37865  islpolN  38012  hdmap1fval  38325  hdmapfval  38356  frlmsnic  38531  uvcn0  38533  ismrc  38638  mzpclval  38662  mzpsubst  38685  mzprename  38686  mzpcompact2lem  38688  eldioph  38695  eldioph2  38699  eldioph2b  38700  eldioph3  38703  rexrabdioph  38732  2rexfrabdioph  38734  3rexfrabdioph  38735  4rexfrabdioph  38736  6rexfrabdioph  38737  7rexfrabdioph  38738  eldioph4i  38750  rabren3dioph  38753  mzpcong  38910  jm2.27dlem1  38947  wepwsolem  38983  aomclem6  39000  aomclem8  39002  dfac11  39003  dgraalem  39086  dgraaub  39089  dgraa0p  39090  mpaaeu  39091  mpaalem  39093  aaitgo  39103  rngunsnply  39114  eliunov2  39332  rfovcnvfvd  39661  fsovfvd  39664  fsovcnvlem  39667  dssmapfv2d  39672  dssmapnvod  39674  clsk1independent  39704  ntrclskb  39727  ntrclsk13  39729  gneispace2  39790  dvconstbi  40026  addrval  40161  subrval  40162  mulvval  40163  fnchoice  40649  refsum2cnlem1  40657  choicefi  40834  axccdom  40858  fmulcl  41239  fmuldfeqlem1  41240  mccllem  41255  mccl  41256  climf  41280  climf2  41324  dvnprodlem1  41607  dvnprodlem3  41609  dvnprod  41610  stoweidlem2  41664  stoweidlem6  41668  stoweidlem8  41670  stoweidlem9  41671  stoweidlem15  41677  stoweidlem16  41678  stoweidlem17  41679  stoweidlem18  41680  stoweidlem21  41683  stoweidlem27  41689  stoweidlem31  41693  stoweidlem36  41698  stoweidlem37  41699  stoweidlem41  41703  stoweidlem43  41705  stoweidlem44  41706  stoweidlem45  41707  stoweidlem46  41708  stoweidlem48  41710  stoweidlem51  41713  stoweidlem55  41717  stoweidlem59  41721  stoweidlem60  41722  stoweidlem62  41724  fourierdlem2  41771  fourierdlem3  41772  elaa2lem  41895  etransclem11  41907  etransclem24  41920  etransclem26  41922  etransclem28  41924  etransclem35  41931  rrndistlt  41952  ioorrnopn  41967  subsaliuncllem  42017  sge0val  42025  ismea  42110  caragenval  42152  isome  42153  isomenndlem  42189  hoicvrrex  42215  ovnlecvr  42217  ovncvrrp  42223  ovn0lem  42224  ovnsubaddlem1  42229  ovnsubadd  42231  hsphoif  42235  hoidmvval  42236  hsphoival  42238  hoidmvlelem3  42256  hoidmvlelem5  42258  hoidmvle  42259  ovnhoilem1  42260  ovnhoi  42262  ovnlecvr2  42269  ovncvr2  42270  hoidifhspval2  42274  hoiqssbllem2  42282  hspmbllem2  42286  hspmbllem3  42287  hspmbl  42288  ovnovollem1  42315  smfmullem2  42444  smfmul  42447  smfpimcclem  42458  iccpart  42894  iccpartiun  42912  icceuelpart  42914  nnsum3primes4  43261  nnsum3primesgbe  43265  nnsum4primesodd  43269  nnsum4primesoddALTV  43270  nnsum4primeseven  43273  nnsum4primesevenALTV  43274  bgoldbtbnd  43282  isomgreqve  43298  isomushgr  43299  isomuspgrlem2  43306  isomgrsym  43309  isomgrtr  43312  ushrisomgr  43314  isupwlk  43319  ismgmhm  43358  isrnghm  43467  lincval  43771  lincdifsn  43786  linindslinci  43810  lindslinindsimp1  43819  linds0  43827  el0ldep  43828  lindsrng01  43830  snlindsntorlem  43832  ldepspr  43835  islindeps2  43845  zlmodzxzldep  43866  offval0  43872  bigoval  43917  elbigo  43919  prelrrx2b  44009  rrx2plord  44015  rrx2vlinest  44036  rrx2linesl  44038  elrrx2linest2  44040  line2ylem  44046  line2xlem  44048  itsclc0  44066  itsclc0b  44067  itscnhlinecirc02p  44080  setrecseq  44095  aacllem  44209