Theorem fveq1 6833

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 5100	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6476	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6500	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6500	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5098  ℩cio 6446  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500

This theorem is referenced by:  fveq1i  6835  fveq1d  6836  iffv  6851  fvmptd3f  6956  fvmptdv2  6959  eqfnun  6982  fsnex  7229  f1prex  7230  isoeq1  7263  oveq  7364  elovmpt3imp  7615  ofrfvalg  7630  offval  7631  offval3  7926  bropopvvv  8032  bropfvvvvlem  8033  poseq  8100  soseq  8101  frrlem1  8228  frrlem13  8240  smoeq  8282  tfrlem12  8320  tz7.44-2  8338  tz7.44-3  8339  rdgeq1  8342  fsetfocdm  8798  fsetprcnex  8799  mapsncnv  8831  elixp2  8839  resixpfo  8874  elixpsn  8875  mapsnend  8973  enfixsn  9014  mapxpen  9071  ac6sfi  9184  ordtypelem7  9429  wemaplem1  9451  ixpiunwdom  9495  oemapval  9592  cantnf  9602  wemapwe  9606  cnfcom3clem  9614  ssttrcl  9624  ttrcltr  9625  ttrclss  9629  ttrclselem2  9635  updjud  9846  infxpenc2lem2  9930  fseqenlem1  9934  dfac8clem  9942  ac5num  9946  acni  9955  acni2  9956  acnlem  9958  dfac4  10032  dfac5lem5  10037  dfac2a  10040  dfac9  10047  dfacacn  10052  dfac12lem1  10054  dfac12r  10057  cofsmo  10179  cfsmolem  10180  cfsmo  10181  cfcoflem  10182  coftr  10183  alephsing  10186  isfin3ds  10239  fin23lem17  10248  fin23lem32  10254  fin23lem39  10260  isf33lem  10276  isf34lem6  10290  axcc2lem  10346  axcc3  10348  axdc2lem  10358  axdc3lem2  10361  axdc3lem3  10362  axdc3  10364  axdc4lem  10365  axcclem  10367  ac6num  10389  axdclem2  10430  konigthlem  10479  inar1  10686  1fv  13563  axdc4uzlem  13906  seqeq3  13929  seqof  13982  ccatfval  14496  wrdl1s1  14538  ccat1st1st  14552  cshf1  14733  cshweqrep  14744  wrdlen2i  14865  wwlktovf  14879  wwlktovf1  14880  wwlktovfo  14881  wrd2f1tovbij  14883  rtrclreclem1  14980  dfrtrclrec2  14981  rtrclreclem2  14982  rtrclreclem4  14984  dfrtrcl2  14985  clim  15417  rlim  15418  ello1  15438  elo1  15449  summo  15640  fsum  15643  prodmo  15859  fprod  15864  bpolylem  15971  bpolyval  15972  vdwlem6  16914  vdwlem8  16916  ramcl  16957  strfvnd  17112  prdsplusgval  17393  prdsmulrval  17395  prdsleval  17397  prdsdsval  17398  prdsvscaval  17399  xpsff1o  17488  isacs2  17576  isnat  17874  yonedalem3b  18202  yonedainv  18204  ischn  18530  chnind  18544  chnub  18545  ismgmhm  18621  ismhm  18710  prdspjmhm  18754  isgrpinv  18923  pwsmulg  19049  isghm  19144  isghmOLD  19145  cayleylem2  19342  symgfix2  19345  gsmsymgrfix  19357  gsmsymgreq  19361  symgfixelq  19362  pmtr3ncomlem2  19403  pmtrdifel  19409  pmtrdifwrdel  19414  pmtrdifwrdel2  19415  psgnunilem2  19424  psgnunilem3  19425  efgsdm  19659  efgredlemd  19673  efgredlem  19676  efgred  19677  efgrelexlema  19678  efgrelexlemb  19679  prdsgsum  19910  pwspjmhmmgpd  20263  pwsexpg  20264  pwsgprod  20265  isrnghm  20377  isabv  20744  islmhm  20979  frgpcyg  21528  psgndiflemB  21555  psgndiflemA  21556  dsmmelbas  21694  frlmipval  21734  frlmphl  21736  uvcf1  21747  islindf  21767  islindf4  21793  psrmulfval  21899  evlslem2  22034  evlslem3  22035  evlslem1  22037  mpfrcl  22040  evlsvval  22045  evlsvvval  22048  selvval  22078  psdval  22102  psdcoef  22103  psdadd  22106  psdmul  22109  psdmvr  22112  coe1fval  22146  coe1mul2lem2  22210  coe1tm  22215  madetsumid  22405  mvmulval  22487  marepvval0  22510  mulmarep1gsum2  22518  mdetleib2  22532  m1detdiag  22541  mdetralt  22552  mdetunilem7  22562  mdetunilem9  22564  m2detleiblem3  22573  m2detleiblem4  22574  m2detleib  22575  symgmatr01lem  22597  gsummatr01lem1  22599  gsummatr01lem4  22602  gsummatr01  22603  smadiadetlem3  22612  pmatcoe1fsupp  22645  pmatcollpw3lem  22727  pmatcollpw3fi1lem2  22731  iscnp  23181  1stcfb  23389  ptpjpre1  23515  elpt  23516  elptr  23517  ptpjopn  23556  dfac14  23562  upxp  23567  pthaus  23582  ptrescn  23583  xkoptsub  23598  cnmptkp  23624  xkofvcn  23628  cnmptk1p  23629  cnmptk2  23630  ptunhmeo  23752  ptcmplem3  23998  ptcmplem4  23999  symgtgp  24050  prdstmdd  24068  isucn  24221  imasdsf1olem  24317  prdsxmslem2  24473  tngngp3  24600  nmoval  24659  elcncf  24838  ishtpy  24927  pcoval  24967  om1elbas  24988  elpi1i  25002  iscau  25232  rrxds  25349  rrxdsfival  25369  ehl1eudisval  25377  ehl2eudisval  25379  mbfi1fseqlem6  25677  mbfi1flimlem  25679  isibl  25722  deg1ldg  26053  deg1leb  26056  elply2  26157  elplyr  26162  ne0p  26168  coeeu  26186  coelem  26187  coeeq  26188  coeidlem  26198  elqaalem3  26285  qaa  26287  iaa  26289  aareccl  26290  aannenlem2  26293  aaliou2  26304  dchrptlem2  27232  dchrpt  27234  dchrsum2  27235  sumdchr2  27237  dchrvmaeq0  27471  rpvmasum2  27479  dchrisum0re  27480  ostth  27606  ltsval  27615  nolesgn2o  27639  nogesgn1o  27641  noresle  27665  nosupprefixmo  27668  noinfprefixmo  27669  nosupcbv  27670  nosupfv  27674  noinfcbv  27685  noinffv  27689  iscgrg  28584  isismt  28606  israg  28769  iseqlg  28939  brbtwn  28972  brbtwn2  28978  colinearalg  28983  axsegconlem1  28990  axsegcon  29000  ax5seglem5  29006  axpasch  29014  axlowdim  29034  axeuclidlem  29035  axcontlem1  29037  axcontlem2  29038  axcontlem5  29041  vtxdgfval  29541  1egrvtxdg1  29583  isewlk  29676  iswlk  29684  uspgr2wlkeq2  29720  iswlkon  29729  isclwlk  29846  iscrct  29863  iscycl  29864  iswwlks  29909  wwlknon  29930  wlkiswwlks2  29948  wwlksnredwwlkn0  29969  wlksnwwlknvbij  29981  wwlksnextproplem3  29984  wwlksnextprop  29985  umgr2wlk  30022  midwwlks2s3  30025  elwwlks2  30042  elwspths2spth  30043  rusgrnumwwlkslem  30045  rusgrnumwwlkb0  30047  rusgrnumwwlks  30050  isclwwlk  30059  clwlkclwwlklem1  30074  clwwlkn1loopb  30118  clwwlkel  30121  clwwlkf  30122  clwwlkf1  30124  isclwwlknon  30166  clwwlknon1  30172  s2elclwwlknon2  30179  clwwlkvbij  30188  uhgr3cyclex  30257  fusgreg2wsplem  30408  fusgr2wsp2nb  30409  fusgreghash2wsp  30413  2clwwlkel  30424  extwwlkfabel  30428  numclwwlk1lem2fv  30431  numclwwlk1lem2  30435  clwwlknonclwlknonf1o  30437  dlwwlknondlwlknonf1o  30440  numclwwlk2lem1  30451  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  ex-fv  30518  isnvlem  30685  islno  30828  nmooval  30838  nmblolbi  30875  isphg  30892  ajmoi  30933  ajval  30936  ubthlem3  30947  htthlem  30992  hcau  31259  hlimi  31263  hosmval  31810  hommval  31811  hodmval  31812  hfsmval  31813  hfmmval  31814  adjmo  31907  nmopval  31931  elcnop  31932  ellnop  31933  elunop  31947  elhmop  31948  nmfnval  31951  elcnfn  31957  ellnfn  31958  adjeu  31964  adjval  31965  eigvecval  31971  eigvalfval  31972  adj1  32008  adjeq  32010  hmopadj2  32016  lnopeq0i  32082  lnopeq  32084  elunop2  32088  lnophm  32094  hmopco  32098  nmbdoplb  32100  nmcoplb  32105  lnopcon  32110  lnfn0  32122  lnfnmul  32123  nmbdfnlb  32125  nmcfnlb  32129  lnfncon  32131  riesz4  32139  riesz1  32140  cnlnadjlem9  32150  cnlnadjeu  32153  cnlnssadj  32155  nmopcoi  32170  bra11  32183  cnvbraval  32185  pjss2coi  32239  pjssdif2i  32249  pjssdif1i  32250  pjclem4  32274  pj3si  32282  pj3cor1i  32284  isst  32288  ishst  32289  stri  32332  hstri  32340  aciunf1lem  32740  ismnt  33065  mgcval  33069  fzo0pmtrlast  33174  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  elrgspn  33328  elrgspnsubrunlem1  33329  linds2eq  33462  elrspunidl  33509  elrspunsn  33510  dfufd2lem  33630  extvfv  33698  extvfvv  33699  extvfvcl  33701  evlvarval  33706  evlextv  33707  mplvrpmga  33710  splysubrg  33718  issply  33719  vietalem  33735  vieta  33736  lbsdiflsp0  33783  fedgmullem1  33786  fedgmullem2  33787  fedgmul  33788  fldextrspunlsplem  33830  fldextrspunlsp  33831  fldext2chn  33885  constrextdg2lem  33905  constrextdg2  33906  lmatval  33970  mdetpmtr1  33980  zarcmplem  34038  ismeas  34356  isrnmeas  34357  cntnevol  34385  carsgval  34460  sitgval  34489  eulerpartleme  34520  eulerpartlemd  34523  eulerpartlemr  34531  eulerpartlemgvv  34533  eulerpart  34539  cndprobval  34590  signstfvneq0  34729  reprsum  34770  reprsuc  34772  reprpmtf1o  34783  reprdifc  34784  breprexp  34790  vtsval  34794  hgt750lemb  34813  hgt750lema  34814  hgt750leme  34815  bnj66  35016  bnj106  35024  bnj125  35028  bnj154  35034  bnj155  35035  bnj526  35044  bnj540  35048  bnj609  35073  bnj611  35074  bnj893  35084  bnj1000  35097  bnj1014  35117  bnj1015  35118  bnj1234  35169  bnj1463  35211  fineqvnttrclse  35280  gblacfnacd  35296  loop1cycl  35331  derangenlem  35365  subfacp1lem3  35376  subfacp1lem5  35378  subfacp1lem6  35379  subfacp1  35380  sconnpht  35423  cnpconn  35424  txpconn  35426  ptpconn  35427  indispconn  35428  connpconn  35429  cvxpconn  35436  cvmliftmo  35478  cvmliftlem14  35491  cvmliftlem15  35492  cvmliftiota  35495  cvmlift2  35510  cvmliftphtlem  35511  cvmlift3lem2  35514  cvmlift3lem6  35518  cvmlift3lem7  35519  cvmlift3lem9  35521  cvmlift3  35522  satfv1lem  35556  satfv1  35557  sategoelfvb  35613  mrsubff1  35708  mrsub0  35710  mrsubccat  35712  mrsubcn  35713  elmsubrn  35722  msubrn  35723  msubco  35725  msubvrs  35754  mclsax  35763  shftvalg  35926  fwddifval  36356  fwddifnval  36357  bj-evalval  37280  unceq  37798  matunitlindflem2  37818  poimirlem17  37838  poimirlem20  37841  poimirlem22  37843  poimirlem23  37844  poimirlem27  37848  poimirlem28  37849  poimirlem30  37851  poimirlem31  37852  poimirlem32  37853  poimir  37854  broucube  37855  voliunnfl  37865  volsupnfl  37866  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  ftc1anclem2  37895  ftc1anclem5  37898  upixp  37930  fdc  37946  isismty  38002  rrnmval  38029  elghomlem2OLD  38087  isrngohom  38166  islfl  39320  isopos  39440  islaut  40343  ispautN  40359  isldil  40370  isltrn  40379  ltrnid  40395  ltrneq2  40408  isdilN  40414  istrnN  40417  trlval  40422  ltrneq3  40468  cdleme50ex  40819  cdleme  40820  cdlemg1a  40830  ltrniotaval  40841  ltrniotavalbN  40844  cdlemeiota  40845  cdlemg2jlemOLDN  40853  cdlemg2fvlem  40854  cdlemg2klem  40855  istendo  41020  tendoplcbv  41035  tendopl  41036  tendoicbv  41053  tendoi  41054  tendoid0  41085  tendo1ne0  41088  cdlemksv2  41107  cdlemkuv2  41127  cdlemk33N  41169  cdlemk34  41170  cdlemk36  41173  cdlemk19u  41230  cdlemk  41234  tendoex  41235  dvavsca  41277  dvhvscacbv  41358  dvhvscaval  41359  dicopelval  41437  dicelval1sta  41447  diclspsn  41454  dihmeetlem13N  41579  dih1dimatlem0  41588  dih1dimatlem  41589  dihpN  41596  islpolN  41743  hdmap1fval  42056  hdmapfval  42087  sticksstones1  42400  sticksstones2  42401  sticksstones3  42402  sticksstones8  42407  sticksstones10  42409  sticksstones11  42410  sticksstones12a  42411  sticksstones12  42412  sticksstones15  42415  frlmsnic  42795  uvcn0  42797  mplmapghm  42807  evlsvarval  42811  evlsbagval  42812  selvvvval  42828  evlselv  42830  fsuppssindlem2  42835  fsuppssind  42836  prjspnfv01  42867  prjspner01  42868  prjspner1  42869  sn-isghm  42916  ismrc  42943  mzpclval  42967  mzpsubst  42990  mzprename  42991  mzpcompact2lem  42993  eldioph  43000  eldioph2  43004  eldioph2b  43005  eldioph3  43008  rexrabdioph  43036  2rexfrabdioph  43038  3rexfrabdioph  43039  4rexfrabdioph  43040  6rexfrabdioph  43041  7rexfrabdioph  43042  eldioph4i  43054  rabren3dioph  43057  mzpcong  43214  jm2.27dlem1  43251  wepwsolem  43284  aomclem6  43301  aomclem8  43303  dfac11  43304  dgraalem  43387  dgraaub  43390  dgraa0p  43391  mpaaeu  43392  mpaalem  43394  aaitgo  43404  rngunsnply  43411  cantnfresb  43566  tfsconcatun  43579  nvocnvb  43663  eliunov2  43920  rfovcnvfvd  44248  fsovfvd  44251  fsovcnvlem  44254  dssmapfv2d  44259  dssmapnvod  44261  clsk1independent  44287  ntrclskb  44310  ntrclsk13  44312  gneispace2  44373  mnringmulrvald  44468  dvconstbi  44575  addrval  44706  subrval  44707  mulvval  44708  relpeq1  45185  fnchoice  45274  refsum2cnlem1  45282  choicefi  45444  axccdom  45466  fmulcl  45827  fmuldfeqlem1  45828  mccllem  45843  mccl  45844  climf  45868  climf2  45910  dvnprodlem1  46190  dvnprodlem3  46192  dvnprod  46193  stoweidlem2  46246  stoweidlem6  46250  stoweidlem8  46252  stoweidlem9  46253  stoweidlem15  46259  stoweidlem16  46260  stoweidlem17  46261  stoweidlem18  46262  stoweidlem21  46265  stoweidlem27  46271  stoweidlem31  46275  stoweidlem36  46280  stoweidlem37  46281  stoweidlem41  46285  stoweidlem43  46287  stoweidlem44  46288  stoweidlem45  46289  stoweidlem46  46290  stoweidlem48  46292  stoweidlem51  46295  stoweidlem55  46299  stoweidlem59  46303  stoweidlem60  46304  stoweidlem62  46306  fourierdlem2  46353  fourierdlem3  46354  elaa2lem  46477  etransclem11  46489  etransclem24  46502  etransclem26  46504  etransclem28  46506  etransclem35  46513  rrndistlt  46534  ioorrnopn  46549  subsaliuncllem  46601  sge0val  46610  ismea  46695  caragenval  46737  isome  46738  isomenndlem  46774  hoicvrrex  46800  ovnlecvr  46802  ovncvrrp  46808  ovn0lem  46809  ovnsubaddlem1  46814  ovnsubadd  46816  hsphoif  46820  hoidmvval  46821  hsphoival  46823  hoidmvlelem3  46841  hoidmvlelem5  46843  hoidmvle  46844  ovnhoilem1  46845  ovnhoi  46847  ovnlecvr2  46854  ovncvr2  46855  hoidifhspval2  46859  hoiqssbllem2  46867  hspmbllem2  46871  hspmbllem3  46872  hspmbl  46873  ovnovollem1  46900  smfmullem2  47036  smfmul  47039  smfpimcclem  47051  chnerlem1  47126  nthrucw  47130  sinnpoly  47137  cfsetsnfsetfv  47303  cfsetsnfsetfo  47306  iccpart  47662  iccpartiun  47680  icceuelpart  47682  nnsum3primes4  48034  nnsum3primesgbe  48038  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  bgoldbtbnd  48055  isisubgr  48108  isgrim  48128  grimidvtxedg  48131  grimcnv  48134  grimco  48135  isuspgrim0  48140  gricushgr  48163  ushggricedg  48173  uhgrimisgrgric  48177  isgrtri  48189  isubgr3stgrlem3  48214  isubgr3stgr  48221  isgrlim  48228  uspgrlim  48238  grlicref  48258  grlicsym  48259  grlictr  48261  grlimedgnedg  48377  isupwlk  48382  lincval  48655  lincdifsn  48670  linindslinci  48694  lindslinindsimp1  48703  linds0  48711  el0ldep  48712  lindsrng01  48714  snlindsntorlem  48716  ldepspr  48719  islindeps2  48729  zlmodzxzldep  48750  bigoval  48795  elbigo  48797  0aryfvalelfv  48881  1arympt1fv  48885  1arymaptfv  48886  1arymaptfo  48889  2arymptfv  48896  2arymaptfv  48897  2arymaptfo  48900  prelrrx2b  48960  rrx2plord  48966  rrx2vlinest  48987  rrx2linesl  48989  elrrx2linest2  48991  line2ylem  48997  line2xlem  48999  itsclc0  49017  itsclc0b  49018  itscnhlinecirc02p  49031  elfvne0  49094  iinfprg  49304  thincciso  49698  thinccisod  49699  setrecseq  49930  aacllem  50046