Theorem fveq1 6190

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 4655	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 5872	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 5896	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 5896	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2681	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1483   class class class wbr 4653  ℩cio 5849  ‘cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896

This theorem is referenced by:  fveq1i  6192  fveq1d  6193  iffv  6205  fvmptd3f  6295  fvmptdv2  6298  fsnex  6538  f1prex  6539  isoeq1  6567  oveq  6656  elovmpt3imp  6890  offval  6904  ofrfval  6905  offval3  7162  bropopvvv  7255  bropfvvvvlem  7256  wfrlem1  7414  wfrlem3a  7417  wfrlem15  7429  smoeq  7447  tfrlem12  7485  tz7.44-2  7503  tz7.44-3  7504  rdgeq1  7507  mapsncnv  7904  elixp2  7912  resixpfo  7946  elixpsn  7947  mapsnen  8035  enfixsn  8069  mapxpen  8126  ac6sfi  8204  ordtypelem7  8429  wemaplem1  8451  ixpiunwdom  8496  oemapval  8580  cantnf  8590  wemapwe  8594  cnfcom3clem  8602  infxpenc2lem2  8843  fseqenlem1  8847  dfac8clem  8855  ac5num  8859  acni  8868  acni2  8869  acnlem  8871  dfac4  8945  dfac5lem5  8950  dfac2a  8952  dfac9  8958  dfacacn  8963  dfac12lem1  8965  dfac12r  8968  cofsmo  9091  cfsmolem  9092  cfsmo  9093  cfcoflem  9094  coftr  9095  alephsing  9098  isfin3ds  9151  fin23lem17  9160  fin23lem32  9166  fin23lem39  9172  isf33lem  9188  isf34lem6  9202  axcc2lem  9258  axcc3  9260  axdc2lem  9270  axdc3lem2  9273  axdc3lem3  9274  axdc3  9276  axdc4lem  9277  axcclem  9279  ac6num  9301  axdclem2  9342  konigthlem  9390  inar1  9597  1fv  12458  axdc4uzlem  12782  seqeq3  12806  seqof  12858  ccatfval  13358  wrdl1s1  13394  cshf1  13556  cshweqrep  13567  wrdlen2i  13686  wwlktovf  13699  wwlktovf1  13700  wwlktovfo  13701  wrd2f1tovbij  13703  dfrtrclrec2  13797  rtrclreclem1  13798  rtrclreclem2  13799  rtrclreclem4  13801  dfrtrcl2  13802  clim  14225  rlim  14226  ello1  14246  elo1  14257  summo  14448  fsum  14451  prodmo  14666  fprod  14671  bpolylem  14779  bpolyval  14780  vdwlem6  15690  vdwlem8  15692  ramcl  15733  strfvnd  15876  prdsplusgval  16133  prdsmulrval  16135  prdsleval  16137  prdsdsval  16138  prdsvscaval  16139  xpsff1o  16228  isacs2  16314  isnat  16607  yonedalem3b  16919  yonedainv  16921  ismhm  17337  prdspjmhm  17367  isgrpinv  17472  pwsmulg  17587  isghm  17660  cayleylem2  17833  symgfix2  17836  gsmsymgrfix  17848  gsmsymgreq  17852  symgfixelq  17853  pmtr3ncomlem2  17894  pmtrdifel  17900  pmtrdifwrdel  17905  pmtrdifwrdel2  17906  psgnunilem2  17915  psgnunilem3  17916  efgsdm  18143  efgredlemd  18157  efgredlem  18160  efgred  18161  efgrelexlema  18162  efgrelexlemb  18163  prdsgsum  18377  isabv  18819  islmhm  19027  psrmulfval  19385  evlslem2  19512  evlslem3  19514  evlslem1  19515  mpfrcl  19518  coe1fval  19575  coe1mul2lem2  19638  coe1tm  19643  frgpcyg  19922  psgndiflemB  19946  psgndiflemA  19947  dsmmelbas  20083  frlmipval  20118  frlmphl  20120  uvcf1  20131  islindf  20151  islindf4  20177  madetsumid  20267  mvmulval  20349  marepvval0  20372  mulmarep1gsum2  20380  mdetleib2  20394  m1detdiag  20403  mdetralt  20414  mdetunilem7  20424  mdetunilem9  20426  m2detleiblem3  20435  m2detleiblem4  20436  m2detleib  20437  symgmatr01lem  20459  gsummatr01lem1  20461  gsummatr01lem4  20464  gsummatr01  20465  smadiadetlem3  20474  pmatcoe1fsupp  20506  pmatcollpw3lem  20588  pmatcollpw3fi1lem2  20592  iscnp  21041  1stcfb  21248  ptpjpre1  21374  elpt  21375  elptr  21376  ptpjopn  21415  dfac14  21421  upxp  21426  pthaus  21441  ptrescn  21442  xkoptsub  21457  cnmptkp  21483  xkofvcn  21487  cnmptk1p  21488  cnmptk2  21489  ptunhmeo  21611  ptcmplem3  21858  ptcmplem4  21859  symgtgp  21905  prdstmdd  21927  isucn  22082  imasdsf1olem  22178  prdsxmslem2  22334  tngngp3  22460  nmoval  22519  elcncf  22692  ishtpy  22771  pcoval  22811  om1elbas  22832  elpi1i  22846  iscau  23074  rrxds  23181  mbfi1fseqlem6  23487  mbfi1flimlem  23489  isibl  23532  deg1ldg  23852  deg1leb  23855  elply2  23952  elplyr  23957  ne0p  23963  coeeu  23981  coelem  23982  coeeq  23983  coeidlem  23993  elqaalem3  24076  qaa  24078  iaa  24080  aareccl  24081  aannenlem2  24084  aaliou2  24095  dchrptlem2  24990  dchrpt  24992  dchrsum2  24993  sumdchr2  24995  dchrvmaeq0  25193  rpvmasum2  25201  dchrisum0re  25202  ostth  25328  iscgrg  25407  isismt  25429  israg  25592  iseqlg  25747  brbtwn  25779  brbtwn2  25785  colinearalg  25790  axsegconlem1  25797  axsegcon  25807  ax5seglem5  25813  axpasch  25821  axlowdim  25841  axeuclidlem  25842  axcontlem1  25844  axcontlem2  25845  axcontlem5  25848  vtxdgfval  26363  1egrvtxdg1  26405  isewlk  26498  iswlk  26506  uspgr2wlkeq2  26543  iswlkon  26553  isclwlk  26669  iscrct  26685  iscycl  26686  iswwlks  26728  wwlknon  26742  wlkiswwlks2  26761  wlkwwlkfun  26781  wlkwwlksur  26783  wlkwwlkbij2  26785  wwlksnredwwlkn0  26791  wlksnwwlknvbij  26803  wwlksnextproplem3  26806  wwlksnextprop  26807  umgr2wlk  26845  wwlks2onv  26847  midwwlks2s3  26860  elwwlks2  26861  elwspths2spth  26862  rusgrnumwwlkslem  26864  rusgrnumwwlkb0  26866  rusgrnumwwlks  26869  isclwwlks  26880  clwlkclwwlklem1  26900  clwwlksel  26914  clwwlksf  26915  clwwlksf1  26917  clwwlksvbij  26922  clwwlksnun  26974  uhgr3cyclex  27042  fusgreg2wsplem  27197  fusgr2wsp2nb  27198  fusgreghash2wsp  27202  numclwwlkovfel2  27216  numclwwlkovgel  27221  extwwlkfab  27223  numclwlk1lem2foa  27224  numclwlk1lem2f  27225  numclwlk1lem2fv  27226  numclwlk1lem2  27230  numclwwlk2lem1  27235  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  numclwwlk6  27248  ex-fv  27300  isnvlem  27465  islno  27608  nmooval  27618  nmblolbi  27655  isphg  27672  ajmoi  27714  ajval  27717  ubthlem3  27728  htthlem  27774  hcau  28041  hlimi  28045  hosmval  28594  hommval  28595  hodmval  28596  hfsmval  28597  hfmmval  28598  adjmo  28691  nmopval  28715  elcnop  28716  ellnop  28717  elunop  28731  elhmop  28732  nmfnval  28735  elcnfn  28741  ellnfn  28742  adjeu  28748  adjval  28749  eigvecval  28755  eigvalfval  28756  adj1  28792  adjeq  28794  hmopadj2  28800  lnopeq0i  28866  lnopeq  28868  elunop2  28872  lnophm  28878  hmopco  28882  nmbdoplb  28884  nmcoplb  28889  lnopcon  28894  lnfn0  28906  lnfnmul  28907  nmbdfnlb  28909  nmcfnlb  28913  lnfncon  28915  riesz4  28923  riesz1  28924  cnlnadjlem9  28934  cnlnadjeu  28937  cnlnssadj  28939  nmopcoi  28954  bra11  28967  cnvbraval  28969  pjss2coi  29023  pjssdif2i  29033  pjssdif1i  29034  pjclem4  29058  pj3si  29066  pj3cor1i  29068  isst  29072  ishst  29073  stri  29116  hstri  29124  aciunf1lem  29462  lmatval  29879  mdetpmtr1  29889  ismeas  30262  isrnmeas  30263  cntnevol  30291  carsgval  30365  sitgval  30394  eulerpartleme  30425  eulerpartlemd  30428  eulerpartlemr  30436  eulerpartlemgvv  30438  eulerpart  30444  cndprobval  30495  signstfvneq0  30649  reprsum  30691  reprsuc  30693  reprpmtf1o  30704  reprdifc  30705  breprexp  30711  vtsval  30715  hgt750lemb  30734  hgt750lema  30735  hgt750leme  30736  bnj66  30930  bnj106  30938  bnj125  30942  bnj154  30948  bnj155  30949  bnj526  30958  bnj540  30962  bnj609  30987  bnj611  30988  bnj893  30998  bnj1000  31011  bnj1014  31030  bnj1015  31031  bnj1234  31081  bnj1463  31123  derangenlem  31153  subfacp1lem3  31164  subfacp1lem5  31166  subfacp1lem6  31167  subfacp1  31168  sconnpht  31211  cnpconn  31212  txpconn  31214  ptpconn  31215  indispconn  31216  connpconn  31217  cvxpconn  31224  cvmliftmo  31266  cvmliftlem14  31279  cvmliftlem15  31280  cvmliftiota  31283  cvmlift2  31298  cvmliftphtlem  31299  cvmlift3lem2  31302  cvmlift3lem6  31306  cvmlift3lem7  31307  cvmlift3lem9  31309  cvmlift3  31310  mrsubff1  31411  mrsub0  31413  mrsubccat  31415  mrsubcn  31416  elmsubrn  31425  msubrn  31426  msubco  31428  msubvrs  31457  mclsax  31466  shftvalg  31617  poseq  31750  soseq  31751  frrlem1  31780  sltval  31800  nolesgn2o  31824  noresle  31846  noprefixmo  31848  nosupfv  31852  fwddifval  32269  fwddifnval  32270  bj-evalval  33027  unceq  33386  matunitlindflem2  33406  poimirlem17  33426  poimirlem20  33429  poimirlem22  33431  poimirlem23  33432  poimirlem27  33436  poimirlem28  33437  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  poimir  33442  broucube  33443  voliunnfl  33453  volsupnfl  33454  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  ftc1anclem2  33486  ftc1anclem5  33489  eqfnun  33516  upixp  33524  fdc  33541  isismty  33600  rrnmval  33627  elghomlem2OLD  33685  isrngohom  33764  islfl  34347  isopos  34467  islaut  35369  ispautN  35385  isldil  35396  isltrn  35405  ltrnid  35421  ltrneq2  35434  isdilN  35441  istrnN  35444  trlval  35449  ltrneq3  35495  cdleme50ex  35847  cdleme  35848  cdlemg1a  35858  ltrniotaval  35869  ltrniotavalbN  35872  cdlemeiota  35873  cdlemg2jlemOLDN  35881  cdlemg2fvlem  35882  cdlemg2klem  35883  istendo  36048  tendoplcbv  36063  tendopl  36064  tendoicbv  36081  tendoi  36082  tendoid0  36113  tendo1ne0  36116  cdlemksv2  36135  cdlemkuv2  36155  cdlemk33N  36197  cdlemk34  36198  cdlemk36  36201  cdlemk19u  36258  cdlemk  36262  tendoex  36263  dvavsca  36305  dvhvscacbv  36387  dvhvscaval  36388  dicopelval  36466  dicelval1sta  36476  diclspsn  36483  dihmeetlem13N  36608  dih1dimatlem0  36617  dih1dimatlem  36618  dihpN  36625  islpolN  36772  hdmap1fval  37086  hdmapfval  37119  ismrc  37264  mzpclval  37288  mzpsubst  37311  mzprename  37312  mzpcompact2lem  37314  eldioph  37321  eldioph2  37325  eldioph2b  37326  eldioph3  37329  rexrabdioph  37358  2rexfrabdioph  37360  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  eldioph4i  37376  rabren3dioph  37379  mzpcong  37539  jm2.27dlem1  37576  wepwsolem  37612  aomclem6  37629  aomclem8  37631  dfac11  37632  dgraalem  37715  dgraaub  37718  dgraa0p  37719  mpaaeu  37720  mpaalem  37722  aaitgo  37732  rngunsnply  37743  eliunov2  37971  rfovcnvfvd  38301  fsovfvd  38304  fsovcnvlem  38307  dssmapfv2d  38312  dssmapnvod  38314  clsk1independent  38344  ntrclskb  38367  ntrclsk13  38369  gneispace2  38430  dvconstbi  38533  addrval  38670  subrval  38671  mulvval  38672  fnchoice  39188  refsum2cnlem1  39196  mapsnend  39391  choicefi  39392  axccdom  39416  fmulcl  39813  fmuldfeqlem1  39814  mccllem  39829  mccl  39830  climf  39854  climf2  39898  dvnprodlem1  40161  dvnprodlem3  40163  dvnprod  40164  stoweidlem2  40219  stoweidlem6  40223  stoweidlem8  40225  stoweidlem9  40226  stoweidlem15  40232  stoweidlem16  40233  stoweidlem17  40234  stoweidlem18  40235  stoweidlem21  40238  stoweidlem27  40244  stoweidlem31  40248  stoweidlem36  40253  stoweidlem37  40254  stoweidlem41  40258  stoweidlem43  40260  stoweidlem44  40261  stoweidlem45  40262  stoweidlem46  40263  stoweidlem48  40265  stoweidlem51  40268  stoweidlem55  40272  stoweidlem59  40276  stoweidlem60  40277  stoweidlem62  40279  fourierdlem2  40326  fourierdlem3  40327  elaa2lem  40450  etransclem11  40462  etransclem24  40475  etransclem26  40477  etransclem28  40479  etransclem35  40486  rrndistlt  40510  ioorrnopn  40525  subsaliuncllem  40575  sge0val  40583  ismea  40668  caragenval  40707  isome  40708  isomenndlem  40744  hoicvrrex  40770  ovnlecvr  40772  ovncvrrp  40778  ovn0lem  40779  ovnsubaddlem1  40784  ovnsubadd  40786  hsphoif  40790  hoidmvval  40791  hsphoival  40793  hoidmvlelem3  40811  hoidmvlelem5  40813  hoidmvle  40814  ovnhoilem1  40815  ovnhoi  40817  ovnlecvr2  40824  ovncvr2  40825  hoidifhspval2  40829  hoiqssbllem2  40837  hspmbllem2  40841  hspmbllem3  40842  hspmbl  40843  ovnovollem1  40870  smfmullem2  40999  smfmul  41002  smfpimcclem  41013  iccpart  41352  iccpartiun  41370  icceuelpart  41372  nnsum3primes4  41676  nnsum3primesgbe  41680  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbnd  41697  isupwlk  41717  ismgmhm  41783  isrnghm  41892  lincval  42198  lincdifsn  42213  linindslinci  42237  lindslinindsimp1  42246  linds0  42254  el0ldep  42255  lindsrng01  42257  snlindsntorlem  42259  ldepspr  42262  islindeps2  42272  zlmodzxzldep  42293  offval0  42299  bigoval  42343  elbigo  42345  setrecseq  42432  aacllem  42547