Theorem fveq1 6915

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 5110	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6549	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6574	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6574	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2823	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5108  ℩cio 6518  ‘cfv 6566

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574

This theorem is used by:  fveq1i  6917  fveq1d  6918  iffv  6933  fvmptd3f  7040  fvmptdv2  7043  eqfnun  7067  fsnex  7322  f1prex  7323  isoeq1  7356  oveq  7457  elovmpt3imp  7710  ofrfvalg  7733  offval  7734  offval3  8028  bropopvvv  8136  bropfvvvvlem  8137  poseq  8212  soseq  8213  frrlem1  8342  frrlem13  8354  smoeq  8396  tfrlem12  8435  tz7.44-2  8453  tz7.44-3  8454  rdgeq1  8457  fsetfocdm  8921  fsetprcnex  8922  mapsncnv  8959  elixp2  8967  resixpfo  9002  elixpsn  9003  mapsnend  9102  enfixsn  9143  mapxpen  9200  ac6sfi  9313  ordtypelem7  9555  wemaplem1  9577  ixpiunwdom  9621  oemapval  9721  cantnf  9731  wemapwe  9735  cnfcom3clem  9743  ssttrcl  9753  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  updjud  10052  infxpenc2lem2  10138  fseqenlem1  10142  dfac8clem  10150  ac5num  10154  acni  10163  acni2  10164  acnlem  10166  dfac4  10240  dfac5lem5  10245  dfac2a  10247  dfac9  10254  dfacacn  10259  dfac12lem1  10261  dfac12r  10264  cofsmo  10386  cfsmolem  10387  cfsmo  10388  cfcoflem  10389  coftr  10390  alephsing  10393  isfin3ds  10446  fin23lem17  10455  fin23lem32  10461  fin23lem39  10467  isf33lem  10483  isf34lem6  10497  axcc2lem  10553  axcc3  10555  axdc2lem  10565  axdc3lem2  10568  axdc3lem3  10569  axdc3  10571  axdc4lem  10572  axcclem  10574  ac6num  10596  axdclem2  10637  konigthlem  10692  inar1  10899  1fv  13821  axdc4uzlem  14166  seqeq3  14189  seqof  14242  ccatfval  14759  wrdl1s1  14804  ccat1st1st  14818  cshf1  15003  cshweqrep  15014  wrdlen2i  15136  wwlktovf  15152  wwlktovf1  15153  wwlktovfo  15154  wrd2f1tovbij  15156  rtrclreclem1  15253  dfrtrclrec2  15254  rtrclreclem2  15255  rtrclreclem4  15257  dfrtrcl2  15258  clim  15705  rlim  15706  ello1  15726  elo1  15737  summo  15927  fsum  15930  prodmo  16147  fprod  16152  bpolylem  16258  bpolyval  16259  vdwlem6  17208  vdwlem8  17210  ramcl  17251  strfvnd  17407  prdsplusgval  17694  prdsmulrval  17696  prdsleval  17698  prdsdsval  17699  prdsvscaval  17700  xpsff1o  17789  isacs2  17877  isnat  18175  yonedalem3b  18503  yonedainv  18505  ischn  18831  chnind  18845  chnub  18846  ismgmhm  18935  ismhm  19030  prdspjmhm  19075  isgrpinv  19254  pwsmulg  19379  isghm  19480  cayleylem2  19678  symgfix2  19681  gsmsymgrfix  19693  gsmsymgreq  19697  symgfixelq  19698  pmtr3ncomlem2  19739  pmtrdifel  19745  pmtrdifwrdel  19750  pmtrdifwrdel2  19751  psgnunilem2  19760  psgnunilem3  19761  efgsdm  19995  efgredlemd  20009  efgredlem  20012  efgred  20013  efgrelexlema  20014  efgrelexlemb  20015  prdsgsum  20246  pwspjmhmmgpd  20608  pwsexpg  20609  pwsgprod  20610  isrnghm  20722  isrhm0  20757  isabv  21119  islmhm  21353  frgpcyg  21934  psgndiflemB  21961  psgndiflemA  21962  dsmmelbas  22100  frlmipval  22140  frlmphl  22142  uvcf1  22153  islindf  22173  islindf4  22199  psrmulfval  22306  evlslem2  22443  evlslem3  22444  evlslem1  22446  mpfrcl  22449  evlsvval  22454  evlsvvval  22457  selvval  22484  mplmapghm  22486  evlsvarval  22491  selvvvval  22506  psdval  22535  psdcoef  22536  psdadd  22539  psdmul  22542  psdmvr  22545  coe1fval  22578  coe1mul2lem2  22642  coe1tm  22647  madetsumid  22831  mvmulval  22913  marepvval0  22936  mulmarep1gsum2  22944  mdetleib2  22958  m1detdiag  22967  mdetralt  22978  mdetunilem7  22988  mdetunilem9  22990  m2detleiblem3  22999  m2detleiblem4  23000  m2detleib  23001  symgmatr01lem  23023  gsummatr01lem1  23025  gsummatr01lem4  23028  gsummatr01  23029  smadiadetlem3  23038  matunitlindflem2  23050  pmatcoe1fsupp  23074  pmatcollpw3lem  23156  pmatcollpw3fi1lem2  23160  iscnp  23610  1stcfb  23818  ptpjpre1  23945  elpt  23946  elptr  23947  ptpjopn  23986  dfac14  23992  upxp  23997  pthaus  24012  ptrescn  24013  xkoptsub  24028  cnmptkp  24054  xkofvcn  24058  cnmptk1p  24059  cnmptk2  24060  ptunhmeo  24182  ptcmplem3  24428  ptcmplem4  24429  symgtgp  24480  prdstmdd  24498  isucn  24651  imasdsf1olem  24747  prdsxmslem2  24903  tngngp3  25030  nmoval  25089  elcncf  25265  ishtpy  25348  pcoval  25387  om1elbas  25408  elpi1i  25422  iscau  25652  rrxds  25769  rrxdsfival  25789  ehl1eudisval  25797  ehl2eudisval  25799  mbfi1fseqlem6  26096  mbfi1flimlem  26098  isibl  26141  deg1ldg  26465  deg1leb  26468  elply2  26569  elplyr  26574  ne0p  26580  coeeu  26599  coelem  26600  coeeq  26601  coeidlem  26611  rngunsnply  26693  elqaalem3  26701  preimaaa  26703  qaa  26704  iaaOLD  26709  aareccl  26710  aannenlem2  26713  aaliou2  26724  dchrptlem2  27649  dchrpt  27651  dchrsum2  27652  sumdchr2  27654  dchrvmaeq0  27888  rpvmasum2  27896  dchrisum0re  27897  ostth  28023  ltsval  28061  nolesgn2o  28085  nogesgn1o  28087  noresle  28111  nosupprefixmo  28114  noinfprefixmo  28115  nosupcbv  28116  nosupfv  28120  noinfcbv  28131  noinffv  28135  iscgrg  29032  isismt  29054  israg  29229  elcgrabasi  29432  elcgrabasrd  29433  cgrabasimass  29435  iseqlg  29469  brbtwn  29534  brbtwn2  29540  colinearalg  29545  axsegconlem1  29552  axsegcon  29562  ax5seglem5  29568  axpasch  29576  axlowdim  29596  axeuclidlem  29597  axcontlem1  29599  axcontlem2  29600  axcontlem5  29603  vtxdgfval  30105  1egrvtxdg1  30147  isewlk  30240  iswlk  30248  uspgr2wlkeq2  30284  iswlkon  30293  isclwlk  30417  iscrct  30434  iscycl  30435  iswwlks  30482  wwlknon  30503  wlkiswwlks2  30521  wwlksnredwwlkn0  30542  wlksnwwlknvbij  30554  wwlksnextproplem3  30557  wwlksnextprop  30558  umgr2wlk  30595  midwwlks2s3  30598  elwwlks2  30615  elwspths2spth  30616  rusgrnumwwlkslem  30618  rusgrnumwwlkb0  30620  rusgrnumwwlks  30623  isclwwlk  30632  clwlkclwwlklem1  30647  clwwlkn1loopb  30691  clwwlkel  30694  clwwlkf  30695  clwwlkf1  30697  isclwwlknon  30739  clwwlknon1  30745  s2elclwwlknon2  30752  clwwlkvbij  30761  loop1cycl  30801  uhgr3cyclex  30840  fusgreg2wsplem  30991  fusgr2wsp2nb  30992  fusgreghash2wsp  30996  2clwwlkel  31007  extwwlkfabel  31011  numclwwlk1lem2fv  31014  numclwwlk1lem2  31018  clwwlknonclwlknonf1o  31020  dlwwlknondlwlknonf1o  31023  numclwwlk2lem1  31034  numclwlk2lem2f  31035  numclwlk2lem2f1o  31037  ex-fv  31101  isnvlem  31269  islno  31412  nmooval  31422  nmblolbi  31459  isphg  31476  ajmoi  31517  ajval  31520  ubthlem3  31531  htthlem  31576  hcau  31843  hlimi  31847  hosmval  32394  hommval  32395  hodmval  32396  hfsmval  32397  hfmmval  32398  adjmo  32491  nmopval  32515  elcnop  32516  ellnop  32517  elunop  32531  elhmop  32532  nmfnval  32535  elcnfn  32541  ellnfn  32542  adjeu  32548  adjval  32549  eigvecval  32555  eigvalfval  32556  adj1  32592  adjeq  32594  hmopadj2  32600  lnopeq0i  32666  lnopeq  32668  elunop2  32672  lnophm  32678  hmopco  32682  nmbdoplb  32684  nmcoplb  32689  lnopcon  32694  lnfn0  32706  lnfnmul  32707  nmbdfnlb  32709  nmcfnlb  32713  lnfncon  32715  riesz4  32723  riesz1  32724  cnlnadjlem9  32734  cnlnadjeu  32737  cnlnssadj  32739  nmopcoi  32754  bra11  32767  cnvbraval  32769  pjss2coi  32823  pjssdif2i  32833  pjssdif1i  32834  pjclem4  32858  pj3si  32866  pj3cor1i  32868  isst  32872  ishst  32873  stri  32916  hstri  32924  aciunf1lem  33354  ismnt  33643  mgcval  33647  fzo0pmtrlast  33752  elrgspnlem1  33902  elrgspnlem2  33903  elrgspnlem3  33904  elrgspnlem4  33905  elrgspn  33906  elrgspnsubrunlem1  33907  linds2eq  34040  elrspunidl  34082  elrspunsn  34083  dfufd2lem  34185  psrnzr  34255  0mplrim  34257  0mplric  34258  selvply1rhmlema  34261  selvply1rhmlemb  34262  selvply1rhmlem1  34263  selvply1rhmlem3  34265  selvply1rhmlem5  34267  selvply1rhm  34268  mplidom  34271  extvfv  34276  extvfvv  34277  extvfvcl  34279  evlvarval  34284  evlextv  34285  mplvrpmga  34288  splysubrg  34303  issply  34304  vietalem  34322  vieta  34323  lbsdiflsp0  34369  fedgmullem1  34372  fedgmullem2  34373  fedgmul  34374  fldextrspunlsplem  34416  fldextrspunlsp  34417  fldext2chn  34471  constrextdg2lem  34491  constrextdg2  34492  lmatval  34556  mdetpmtr1  34566  zarcmplem  34624  ismeas  34943  isrnmeas  34944  cntnevol  34972  carsgval  35046  sitgval  35075  eulerpartleme  35106  eulerpartlemd  35109  eulerpartlemr  35117  eulerpartlemgvv  35119  eulerpart  35125  cndprobval  35176  signstfvneq0  35312  reprsum  35353  reprsuc  35355  reprpmtf1o  35366  reprdifc  35367  breprexp  35373  vtsval  35377  hgt750lemb  35396  hgt750lema  35397  hgt750leme  35398  bnj66  35601  bnj106  35609  bnj125  35613  bnj154  35619  bnj155  35620  bnj526  35629  bnj540  35633  bnj609  35658  bnj611  35659  bnj893  35669  bnj1000  35682  bnj1014  35702  bnj1015  35703  bnj1234  35754  bnj1463  35796  fineqvnttrclse  35933  gblacfnacd  36070  srepdflem2  36127  srepdf  36128  derangenlem  36144  subfacp1lem3  36155  subfacp1lem5  36157  subfacp1lem6  36158  subfacp1  36159  sconnpht  36202  cnpconn  36203  txpconn  36205  ptpconn  36206  indispconn  36207  connpconn  36208  cvxpconn  36215  cvmliftmo  36257  cvmliftlem14  36270  cvmliftlem15  36271  cvmliftiota  36274  cvmlift2  36289  cvmliftphtlem  36290  cvmlift3lem2  36293  cvmlift3lem6  36297  cvmlift3lem7  36298  cvmlift3lem9  36300  cvmlift3  36301  satfv1lem  36335  satfv1  36336  sategoelfvb  36392  mrsubff1  36487  mrsub0  36489  mrsubccat  36491  mrsubcn  36492  elmsubrn  36501  msubrn  36502  msubco  36504  msubvrs  36533  mclsax  36542  mirimanoffr  36668  shftvalg  36712  fwddifval  37142  fwddifnval  37143  bj-evalval  38266  unceq  38792  poimirlem17  38823  poimirlem20  38826  poimirlem22  38828  poimirlem23  38829  poimirlem27  38833  poimirlem28  38834  poimirlem30  38836  poimirlem31  38837  poimirlem32  38838  poimir  38839  broucube  38840  voliunnfl  38850  volsupnfl  38851  itg2addnclem  38857  itg2addnclem3  38859  itg2addnc  38860  ftc1anclem2  38880  ftc1anclem5  38883  upixp  38931  fdc  38945  isismty  39001  rrnmval  39028  elghomlem2OLD  39086  isrngohom  39165  islfl  40383  isopos  40503  islaut  41406  ispautN  41422  isldil  41433  isltrn  41442  ltrnid  41458  ltrneq2  41471  isdilN  41477  istrnN  41480  trlval  41485  ltrneq3  41531  cdleme50ex  41882  cdleme  41883  cdlemg1a  41893  ltrniotaval  41904  ltrniotavalbN  41907  cdlemeiota  41908  cdlemg2jlemOLDN  41916  cdlemg2fvlem  41917  cdlemg2klem  41918  istendo  42083  tendoplcbv  42098  tendopl  42099  tendoicbv  42116  tendoi  42117  tendoid0  42148  tendo1ne0  42151  cdlemksv2  42170  cdlemkuv2  42190  cdlemk33N  42232  cdlemk34  42233  cdlemk36  42236  cdlemk19u  42293  cdlemk  42297  tendoex  42298  dvavsca  42340  dvhvscacbv  42421  dvhvscaval  42422  dicopelval  42500  dicelval1sta  42510  diclspsn  42517  dihmeetlem13N  42642  dih1dimatlem0  42651  dih1dimatlem  42652  dihpN  42659  islpolN  42806  hdmap1fval  43119  hdmapfval  43150  sticksstones1  43462  sticksstones2  43463  sticksstones3  43464  sticksstones8  43469  sticksstones10  43471  sticksstones11  43472  sticksstones12a  43473  sticksstones12  43474  sticksstones15  43477  frlmsnic  43870  uvcn0  43872  evlsbagval  43880  evlselv  43883  fsuppssindlem2  43886  fsuppssind  43887  frlmnzcoordval  43919  sn-isghm  43950  ismrc  43978  mzpclval  44002  mzpsubst  44025  mzprename  44026  mzpcompact2lem  44028  eldioph  44035  eldioph2  44039  eldioph2b  44040  eldioph3  44043  rexrabdioph  44067  2rexfrabdioph  44069  3rexfrabdioph  44070  4rexfrabdioph  44071  6rexfrabdioph  44072  7rexfrabdioph  44073  eldioph4i  44085  rabren3dioph  44088  mzpcong  44245  jm2.27dlem1  44282  wepwsolem  44315  aomclem6  44327  aomclem8  44329  dfac11  44330  dgraalem  44412  dgraaub  44415  dgraa0p  44416  mpaaeu  44417  mpaalem  44419  aaitgo  44429  cantnfresb  44587  tfsconcatun  44600  nvocnvb  44684  eliunov2  44940  rfovcnvfvd  45268  fsovfvd  45271  fsovcnvlem  45274  dssmapfv2d  45279  dssmapnvod  45281  clsk1independent  45307  ntrclskb  45330  ntrclsk13  45332  gneispace2  45393  mnringmulrvald  45486  dvconstbi  45579  addrval  45708  subrval  45709  mulvval  45710  relpeq1  46198  fnchoice  46320  refsum2cnlem1  46328  choicefi  46487  axccdom  46508  fmulcl  46866  fmuldfeqlem1  46867  mccllem  46882  mccl  46883  climf  46907  climf2  46949  dvnprodlem1  47229  dvnprodlem3  47231  dvnprod  47232  stoweidlem2  47285  stoweidlem6  47289  stoweidlem8  47291  stoweidlem9  47292  stoweidlem15  47298  stoweidlem16  47299  stoweidlem17  47300  stoweidlem18  47301  stoweidlem21  47304  stoweidlem27  47310  stoweidlem31  47314  stoweidlem36  47319  stoweidlem37  47320  stoweidlem41  47324  stoweidlem43  47326  stoweidlem44  47327  stoweidlem45  47328  stoweidlem46  47329  stoweidlem48  47331  stoweidlem51  47334  stoweidlem55  47338  stoweidlem59  47342  stoweidlem60  47343  stoweidlem62  47345  fourierdlem2  47392  fourierdlem3  47393  elaa2lem  47516  etransclem11  47528  etransclem24  47541  etransclem26  47543  etransclem28  47545  etransclem35  47552  rrndistlt  47573  ioorrnopn  47588  subsaliuncllem  47640  sge0val  47649  ismea  47734  caragenval  47776  isome  47777  isomenndlem  47813  hoicvrrex  47839  ovnlecvr  47841  ovncvrrp  47847  ovn0lem  47848  ovnsubaddlem1  47853  ovnsubadd  47855  hsphoif  47859  hoidmvval  47860  hsphoival  47862  hoidmvlelem3  47880  hoidmvlelem5  47882  hoidmvle  47883  ovnhoilem1  47884  ovnhoi  47886  ovnlecvr2  47893  ovncvr2  47894  hoidifhspval2  47898  hoiqssbllem2  47906  hspmbllem2  47910  hspmbllem3  47911  hspmbl  47912  ovnovollem1  47939  smfmullem2  48075  smfmul  48078  smfpimcclem  48090  chnerlem1  48165  sqrtnnaa  48186  sqrtnzqaa  48187  sinnpoly  48214  cfsetsnfsetfv  48400  cfsetsnfsetfo  48403  iccpart  48771  iccpartiun  48789  icceuelpart  48791  nnsum3primes4  49159  nnsum3primesgbe  49163  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  bgoldbtbnd  49180  isisubgr  49233  isgrim  49253  grimidvtxedg  49256  grimcnv  49259  grimco  49260  isuspgrim0  49265  gricushgr  49288  ushggricedg  49298  uhgrimisgrgric  49302  isgrtri  49314  isubgr3stgrlem3  49339  isubgr3stgr  49346  isgrlim  49353  uspgrlim  49363  grlicref  49383  grlicsym  49384  grlictr  49386  grlimedgnedg  49502  isupwlk  49507  linply  49713  lazssaz  49730  lincval  49852  lincdifsn  49867  linindslinci  49891  lindslinindsimp1  49900  linds0  49908  el0ldep  49909  lindsrng01  49911  snlindsntorlem  49913  ldepspr  49916  islindeps2  49926  zlmodzxzldep  49947  bigoval  49992  elbigo  49994  0aryfvalelfv  50078  1arympt1fv  50082  1arymaptfv  50083  1arymaptfo  50086  2arymptfv  50093  2arymaptfv  50094  2arymaptfo  50097  rrx2plord  50164  rrx2vlinest  50184  rrx2linesl  50186  elrrx2linest2  50188  line2ylem  50194  line2xlem  50196  itsclc0  50214  itsclc0b  50215  itscnhlinecirc02p  50228  elfvne0  50291  iinfprg  50504  thincciso  50919  thinccisod  50920  fuconuniqlem  51112  setrecseq  51194  aacllem  51367  crosspval  51382  crosspdot0lem  51391  veronesevald  51399