Theorem fveq1 6889

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

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

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 3897  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551

This theorem is used by:  fveq1i  6891  fveq1d  6892  iffv  6907  fvmptd3f  7014  fvmptdv2  7017  eqfnun  7041  fsnex  7295  f1prex  7296  isoeq1  7329  oveq  7430  elovmpt3imp  7682  ofrfvalg  7705  offval  7706  offval3  7998  bropopvvv  8106  bropfvvvvlem  8107  poseq  8182  soseq  8183  frrlem1  8312  frrlem13  8324  smoeq  8366  tfrlem12  8405  tz7.44-2  8423  tz7.44-3  8424  rdgeq1  8427  fsetfocdm  8891  fsetprcnex  8892  mapsncnv  8929  elixp2  8937  resixpfo  8972  elixpsn  8973  mapsnend  9072  enfixsn  9113  mapxpen  9170  ac6sfi  9283  ordtypelem7  9525  wemaplem1  9547  ixpiunwdom  9591  oemapval  9691  cantnf  9701  wemapwe  9705  cnfcom3clem  9713  ssttrcl  9723  ttrcltr  9724  ttrclss  9728  ttrclselem2  9734  updjud  10022  infxpenc2lem2  10106  fseqenlem1  10110  dfac8clem  10118  ac5num  10122  acni  10131  acni2  10132  acnlem  10134  dfac4  10208  dfac5lem5  10213  dfac2a  10215  dfac9  10222  dfacacn  10227  dfac12lem1  10229  dfac12r  10232  cofsmo  10354  cfsmolem  10355  cfsmo  10356  cfcoflem  10357  coftr  10358  alephsing  10361  isfin3ds  10414  fin23lem17  10423  fin23lem32  10429  fin23lem39  10435  isf33lem  10451  isf34lem6  10465  axcc2lem  10521  axcc3  10523  axdc2lem  10533  axdc3lem2  10536  axdc3lem3  10537  axdc3  10539  axdc4lem  10540  axcclem  10542  ac6num  10564  axdclem2  10605  konigthlem  10660  inar1  10867  1fv  13788  axdc4uzlem  14133  seqeq3  14156  seqof  14209  ccatfval  14725  wrdl1s1  14770  ccat1st1st  14784  cshf1  14969  cshweqrep  14980  wrdlen2i  15102  wwlktovf  15118  wwlktovf1  15119  wwlktovfo  15120  wrd2f1tovbij  15122  rtrclreclem1  15219  dfrtrclrec2  15220  rtrclreclem2  15221  rtrclreclem4  15223  dfrtrcl2  15224  clim  15670  rlim  15671  ello1  15691  elo1  15702  summo  15892  fsum  15895  prodmo  16112  fprod  16117  bpolylem  16223  bpolyval  16224  vdwlem6  17173  vdwlem8  17175  ramcl  17216  strfvnd  17372  prdsplusgval  17653  prdsmulrval  17655  prdsleval  17657  prdsdsval  17658  prdsvscaval  17659  xpsff1o  17748  isacs2  17836  isnat  18134  yonedalem3b  18462  yonedainv  18464  ischn  18790  chnind  18804  chnub  18805  ismgmhm  18894  ismhm  18989  prdspjmhm  19034  isgrpinv  19213  pwsmulg  19338  isghm  19439  cayleylem2  19636  symgfix2  19639  gsmsymgrfix  19651  gsmsymgreq  19655  symgfixelq  19656  pmtr3ncomlem2  19697  pmtrdifel  19703  pmtrdifwrdel  19708  pmtrdifwrdel2  19709  psgnunilem2  19718  psgnunilem3  19719  efgsdm  19953  efgredlemd  19967  efgredlem  19970  efgred  19971  efgrelexlema  19972  efgrelexlemb  19973  prdsgsum  20204  pwspjmhmmgpd  20566  pwsexpg  20567  pwsgprod  20568  isrnghm  20680  isrhm0  20715  isabv  21077  islmhm  21311  frgpcyg  21888  psgndiflemB  21915  psgndiflemA  21916  dsmmelbas  22054  frlmipval  22094  frlmphl  22096  uvcf1  22107  islindf  22127  islindf4  22153  psrmulfval  22260  evlslem2  22397  evlslem3  22398  evlslem1  22400  mpfrcl  22403  evlsvval  22408  evlsvvval  22411  selvval  22438  mplmapghm  22440  evlsvarval  22445  selvvvval  22460  psdval  22489  psdcoef  22490  psdadd  22493  psdmul  22496  psdmvr  22499  coe1fval  22532  coe1mul2lem2  22596  coe1tm  22601  madetsumid  22785  mvmulval  22867  marepvval0  22890  mulmarep1gsum2  22898  mdetleib2  22912  m1detdiag  22921  mdetralt  22932  mdetunilem7  22942  mdetunilem9  22944  m2detleiblem3  22953  m2detleiblem4  22954  m2detleib  22955  symgmatr01lem  22977  gsummatr01lem1  22979  gsummatr01lem4  22982  gsummatr01  22983  smadiadetlem3  22992  matunitlindflem2  23004  pmatcoe1fsupp  23028  pmatcollpw3lem  23110  pmatcollpw3fi1lem2  23114  iscnp  23564  1stcfb  23772  ptpjpre1  23899  elpt  23900  elptr  23901  ptpjopn  23940  dfac14  23946  upxp  23951  pthaus  23966  ptrescn  23967  xkoptsub  23982  cnmptkp  24008  xkofvcn  24012  cnmptk1p  24013  cnmptk2  24014  ptunhmeo  24136  ptcmplem3  24382  ptcmplem4  24383  symgtgp  24434  prdstmdd  24452  isucn  24605  imasdsf1olem  24701  prdsxmslem2  24857  tngngp3  24984  nmoval  25043  elcncf  25219  ishtpy  25302  pcoval  25341  om1elbas  25362  elpi1i  25376  iscau  25606  rrxds  25723  rrxdsfival  25743  ehl1eudisval  25751  ehl2eudisval  25753  mbfi1fseqlem6  26050  mbfi1flimlem  26052  isibl  26095  deg1ldg  26419  deg1leb  26422  elply2  26523  elplyr  26528  ne0p  26534  coeeu  26553  coelem  26554  coeeq  26555  coeidlem  26565  elqaalem3  26653  preimaaa  26655  qaa  26656  iaaOLD  26661  aareccl  26662  aannenlem2  26665  aaliou2  26676  dchrptlem2  27601  dchrpt  27603  dchrsum2  27604  sumdchr2  27606  dchrvmaeq0  27840  rpvmasum2  27848  dchrisum0re  27849  ostth  27975  ltsval  28013  nolesgn2o  28037  nogesgn1o  28039  noresle  28063  nosupprefixmo  28066  noinfprefixmo  28067  nosupcbv  28068  nosupfv  28072  noinfcbv  28083  noinffv  28087  iscgrg  28984  isismt  29006  israg  29181  elcgrabasi  29384  elcgrabasrd  29385  cgrabasimass  29387  iseqlg  29421  brbtwn  29486  brbtwn2  29492  colinearalg  29497  axsegconlem1  29504  axsegcon  29514  ax5seglem5  29520  axpasch  29528  axlowdim  29548  axeuclidlem  29549  axcontlem1  29551  axcontlem2  29552  axcontlem5  29555  vtxdgfval  30057  1egrvtxdg1  30099  isewlk  30192  iswlk  30200  uspgr2wlkeq2  30236  iswlkon  30245  isclwlk  30369  iscrct  30386  iscycl  30387  iswwlks  30434  wwlknon  30455  wlkiswwlks2  30473  wwlksnredwwlkn0  30494  wlksnwwlknvbij  30506  wwlksnextproplem3  30509  wwlksnextprop  30510  umgr2wlk  30547  midwwlks2s3  30550  elwwlks2  30567  elwspths2spth  30568  rusgrnumwwlkslem  30570  rusgrnumwwlkb0  30572  rusgrnumwwlks  30575  isclwwlk  30584  clwlkclwwlklem1  30599  clwwlkn1loopb  30643  clwwlkel  30646  clwwlkf  30647  clwwlkf1  30649  isclwwlknon  30691  clwwlknon1  30697  s2elclwwlknon2  30704  clwwlkvbij  30713  loop1cycl  30753  uhgr3cyclex  30792  fusgreg2wsplem  30943  fusgr2wsp2nb  30944  fusgreghash2wsp  30948  2clwwlkel  30959  extwwlkfabel  30963  numclwwlk1lem2fv  30966  numclwwlk1lem2  30970  clwwlknonclwlknonf1o  30972  dlwwlknondlwlknonf1o  30975  numclwwlk2lem1  30986  numclwlk2lem2f  30987  numclwlk2lem2f1o  30989  ex-fv  31053  isnvlem  31221  islno  31364  nmooval  31374  nmblolbi  31411  isphg  31428  ajmoi  31469  ajval  31472  ubthlem3  31483  htthlem  31528  hcau  31795  hlimi  31799  hosmval  32346  hommval  32347  hodmval  32348  hfsmval  32349  hfmmval  32350  adjmo  32443  nmopval  32467  elcnop  32468  ellnop  32469  elunop  32483  elhmop  32484  nmfnval  32487  elcnfn  32493  ellnfn  32494  adjeu  32500  adjval  32501  eigvecval  32507  eigvalfval  32508  adj1  32544  adjeq  32546  hmopadj2  32552  lnopeq0i  32618  lnopeq  32620  elunop2  32624  lnophm  32630  hmopco  32634  nmbdoplb  32636  nmcoplb  32641  lnopcon  32646  lnfn0  32658  lnfnmul  32659  nmbdfnlb  32661  nmcfnlb  32665  lnfncon  32667  riesz4  32675  riesz1  32676  cnlnadjlem9  32686  cnlnadjeu  32689  cnlnssadj  32691  nmopcoi  32706  bra11  32719  cnvbraval  32721  pjss2coi  32775  pjssdif2i  32785  pjssdif1i  32786  pjclem4  32810  pj3si  32818  pj3cor1i  32820  isst  32824  ishst  32825  stri  32868  hstri  32876  aciunf1lem  33307  ismnt  33594  mgcval  33598  fzo0pmtrlast  33703  elrgspnlem1  33853  elrgspnlem2  33854  elrgspnlem3  33855  elrgspnlem4  33856  elrgspn  33857  elrgspnsubrunlem1  33858  linds2eq  33986  elrspunidl  34028  elrspunsn  34029  dfufd2lem  34131  psrnzr  34194  0mplrim  34196  0mplric  34197  selvply1rhmlema  34200  selvply1rhmlemb  34201  selvply1rhmlem1  34202  selvply1rhmlem3  34204  selvply1rhmlem5  34206  selvply1rhm  34207  mplidom  34210  extvfv  34215  extvfvv  34216  extvfvcl  34218  evlvarval  34223  evlextv  34224  mplvrpmga  34227  splysubrg  34242  issply  34243  vietalem  34261  vieta  34262  lbsdiflsp0  34308  fedgmullem1  34311  fedgmullem2  34312  fedgmul  34313  fldextrspunlsplem  34355  fldextrspunlsp  34356  fldext2chn  34410  constrextdg2lem  34430  constrextdg2  34431  lmatval  34495  mdetpmtr1  34505  zarcmplem  34563  ismeas  34882  isrnmeas  34883  cntnevol  34911  carsgval  34985  sitgval  35014  eulerpartleme  35045  eulerpartlemd  35048  eulerpartlemr  35056  eulerpartlemgvv  35058  eulerpart  35064  cndprobval  35115  signstfvneq0  35251  reprsum  35292  reprsuc  35294  reprpmtf1o  35305  reprdifc  35306  breprexp  35312  vtsval  35316  hgt750lemb  35335  hgt750lema  35336  hgt750leme  35337  bnj66  35540  bnj106  35548  bnj125  35552  bnj154  35558  bnj155  35559  bnj526  35568  bnj540  35572  bnj609  35597  bnj611  35598  bnj893  35608  bnj1000  35621  bnj1014  35641  bnj1015  35642  bnj1234  35693  bnj1463  35735  fineqvnttrclse  35860  gblacfnacd  35980  srepdflem2  36037  srepdf  36038  derangenlem  36054  subfacp1lem3  36065  subfacp1lem5  36067  subfacp1lem6  36068  subfacp1  36069  sconnpht  36112  cnpconn  36113  txpconn  36115  ptpconn  36116  indispconn  36117  connpconn  36118  cvxpconn  36125  cvmliftmo  36167  cvmliftlem14  36180  cvmliftlem15  36181  cvmliftiota  36184  cvmlift2  36199  cvmliftphtlem  36200  cvmlift3lem2  36203  cvmlift3lem6  36207  cvmlift3lem7  36208  cvmlift3lem9  36210  cvmlift3  36211  satfv1lem  36245  satfv1  36246  sategoelfvb  36302  mrsubff1  36397  mrsub0  36399  mrsubccat  36401  mrsubcn  36402  elmsubrn  36411  msubrn  36412  msubco  36414  msubvrs  36443  mclsax  36452  mirimanoffr  36578  shftvalg  36621  fwddifval  37051  fwddifnval  37052  bj-evalval  38132  unceq  38661  poimirlem17  38692  poimirlem20  38695  poimirlem22  38697  poimirlem23  38698  poimirlem27  38702  poimirlem28  38703  poimirlem30  38705  poimirlem31  38706  poimirlem32  38707  poimir  38708  broucube  38709  voliunnfl  38719  volsupnfl  38720  itg2addnclem  38726  itg2addnclem3  38728  itg2addnc  38729  ftc1anclem2  38749  ftc1anclem5  38752  upixp  38800  fdc  38816  isismty  38872  rrnmval  38899  elghomlem2OLD  38957  isrngohom  39036  islfl  40254  isopos  40374  islaut  41277  ispautN  41293  isldil  41304  isltrn  41313  ltrnid  41329  ltrneq2  41342  isdilN  41348  istrnN  41351  trlval  41356  ltrneq3  41402  cdleme50ex  41753  cdleme  41754  cdlemg1a  41764  ltrniotaval  41775  ltrniotavalbN  41778  cdlemeiota  41779  cdlemg2jlemOLDN  41787  cdlemg2fvlem  41788  cdlemg2klem  41789  istendo  41954  tendoplcbv  41969  tendopl  41970  tendoicbv  41987  tendoi  41988  tendoid0  42019  tendo1ne0  42022  cdlemksv2  42041  cdlemkuv2  42061  cdlemk33N  42103  cdlemk34  42104  cdlemk36  42107  cdlemk19u  42164  cdlemk  42168  tendoex  42169  dvavsca  42211  dvhvscacbv  42292  dvhvscaval  42293  dicopelval  42371  dicelval1sta  42381  diclspsn  42388  dihmeetlem13N  42513  dih1dimatlem0  42522  dih1dimatlem  42523  dihpN  42530  islpolN  42677  hdmap1fval  42990  hdmapfval  43021  sticksstones1  43333  sticksstones2  43334  sticksstones3  43335  sticksstones8  43340  sticksstones10  43342  sticksstones11  43343  sticksstones12a  43344  sticksstones12  43345  sticksstones15  43348  frlmsnic  43741  uvcn0  43743  evlsbagval  43751  evlselv  43754  fsuppssindlem2  43757  fsuppssind  43758  frlmnzcoordval  43790  sn-isghm  43821  ismrc  43849  mzpclval  43873  mzpsubst  43896  mzprename  43897  mzpcompact2lem  43899  eldioph  43906  eldioph2  43910  eldioph2b  43911  eldioph3  43914  rexrabdioph  43938  2rexfrabdioph  43940  3rexfrabdioph  43941  4rexfrabdioph  43942  6rexfrabdioph  43943  7rexfrabdioph  43944  eldioph4i  43956  rabren3dioph  43959  mzpcong  44116  jm2.27dlem1  44153  wepwsolem  44186  aomclem6  44198  aomclem8  44200  dfac11  44201  dgraalem  44284  dgraaub  44287  dgraa0p  44288  mpaaeu  44289  mpaalem  44291  aaitgo  44301  rngunsnply  44308  cantnfresb  44463  tfsconcatun  44476  nvocnvb  44560  eliunov2  44816  rfovcnvfvd  45144  fsovfvd  45147  fsovcnvlem  45150  dssmapfv2d  45155  dssmapnvod  45157  clsk1independent  45183  ntrclskb  45206  ntrclsk13  45208  gneispace2  45269  mnringmulrvald  45362  dvconstbi  45455  addrval  45584  subrval  45585  mulvval  45586  relpeq1  46070  fnchoice  46182  refsum2cnlem1  46190  choicefi  46350  axccdom  46371  fmulcl  46729  fmuldfeqlem1  46730  mccllem  46745  mccl  46746  climf  46770  climf2  46812  dvnprodlem1  47092  dvnprodlem3  47094  dvnprod  47095  stoweidlem2  47148  stoweidlem6  47152  stoweidlem8  47154  stoweidlem9  47155  stoweidlem15  47161  stoweidlem16  47162  stoweidlem17  47163  stoweidlem18  47164  stoweidlem21  47167  stoweidlem27  47173  stoweidlem31  47177  stoweidlem36  47182  stoweidlem37  47183  stoweidlem41  47187  stoweidlem43  47189  stoweidlem44  47190  stoweidlem45  47191  stoweidlem46  47192  stoweidlem48  47194  stoweidlem51  47197  stoweidlem55  47201  stoweidlem59  47205  stoweidlem60  47206  stoweidlem62  47208  fourierdlem2  47255  fourierdlem3  47256  elaa2lem  47379  etransclem11  47391  etransclem24  47404  etransclem26  47406  etransclem28  47408  etransclem35  47415  rrndistlt  47436  ioorrnopn  47451  subsaliuncllem  47503  sge0val  47512  ismea  47597  caragenval  47639  isome  47640  isomenndlem  47676  hoicvrrex  47702  ovnlecvr  47704  ovncvrrp  47710  ovn0lem  47711  ovnsubaddlem1  47716  ovnsubadd  47718  hsphoif  47722  hoidmvval  47723  hsphoival  47725  hoidmvlelem3  47743  hoidmvlelem5  47745  hoidmvle  47746  ovnhoilem1  47747  ovnhoi  47749  ovnlecvr2  47756  ovncvr2  47757  hoidifhspval2  47761  hoiqssbllem2  47769  hspmbllem2  47773  hspmbllem3  47774  hspmbl  47775  ovnovollem1  47802  smfmullem2  47938  smfmul  47941  smfpimcclem  47953  chnerlem1  48028  sqrtnnaa  48049  sqrtnzqaa  48050  sinnpoly  48077  cfsetsnfsetfv  48263  cfsetsnfsetfo  48266  iccpart  48634  iccpartiun  48652  icceuelpart  48654  nnsum3primes4  49022  nnsum3primesgbe  49026  nnsum4primesodd  49030  nnsum4primesoddALTV  49031  nnsum4primeseven  49034  nnsum4primesevenALTV  49035  bgoldbtbnd  49043  isisubgr  49096  isgrim  49116  grimidvtxedg  49119  grimcnv  49122  grimco  49123  isuspgrim0  49128  gricushgr  49151  ushggricedg  49161  uhgrimisgrgric  49165  isgrtri  49177  isubgr3stgrlem3  49202  isubgr3stgr  49209  isgrlim  49216  uspgrlim  49226  grlicref  49246  grlicsym  49247  grlictr  49249  grlimedgnedg  49365  isupwlk  49370  lincval  49657  lincdifsn  49672  linindslinci  49696  lindslinindsimp1  49705  linds0  49713  el0ldep  49714  lindsrng01  49716  snlindsntorlem  49718  ldepspr  49721  islindeps2  49731  zlmodzxzldep  49752  bigoval  49797  elbigo  49799  0aryfvalelfv  49883  1arympt1fv  49887  1arymaptfv  49888  1arymaptfo  49891  2arymptfv  49898  2arymaptfv  49899  2arymaptfo  49902  rrx2plord  49969  rrx2vlinest  49989  rrx2linesl  49991  elrrx2linest2  49993  line2ylem  49999  line2xlem  50001  itsclc0  50019  itsclc0b  50020  itscnhlinecirc02p  50033  elfvne0  50096  iinfprg  50309  thincciso  50724  thinccisod  50725  fuconuniqlem  50917  setrecseq  50999  aacllem  51150  crosspval  51165  crosspdot0lem  51174  veronesevald  51182