Theorem fveq1 6857

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 5109	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6495	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6519	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6519	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5107  ℩cio 6462  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519

This theorem is referenced by:  fveq1i  6859  fveq1d  6860  iffv  6875  fvmptd3f  6983  fvmptdv2  6986  eqfnun  7009  fsnex  7258  f1prex  7259  isoeq1  7292  oveq  7393  elovmpt3imp  7646  ofrfvalg  7661  offval  7662  offval3  7961  bropopvvv  8069  bropfvvvvlem  8070  poseq  8137  soseq  8138  frrlem1  8265  frrlem13  8277  smoeq  8319  tfrlem12  8357  tz7.44-2  8375  tz7.44-3  8376  rdgeq1  8379  fsetfocdm  8834  fsetprcnex  8835  mapsncnv  8866  elixp2  8874  resixpfo  8909  elixpsn  8910  mapsnend  9007  enfixsn  9050  mapxpen  9107  ac6sfi  9231  ordtypelem7  9477  wemaplem1  9499  ixpiunwdom  9543  oemapval  9636  cantnf  9646  wemapwe  9650  cnfcom3clem  9658  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  ttrclselem2  9679  updjud  9887  infxpenc2lem2  9973  fseqenlem1  9977  dfac8clem  9985  ac5num  9989  acni  9998  acni2  9999  acnlem  10001  dfac4  10075  dfac5lem5  10080  dfac2a  10083  dfac9  10090  dfacacn  10095  dfac12lem1  10097  dfac12r  10100  cofsmo  10222  cfsmolem  10223  cfsmo  10224  cfcoflem  10225  coftr  10226  alephsing  10229  isfin3ds  10282  fin23lem17  10291  fin23lem32  10297  fin23lem39  10303  isf33lem  10319  isf34lem6  10333  axcc2lem  10389  axcc3  10391  axdc2lem  10401  axdc3lem2  10404  axdc3lem3  10405  axdc3  10407  axdc4lem  10408  axcclem  10410  ac6num  10432  axdclem2  10473  konigthlem  10521  inar1  10728  1fv  13608  axdc4uzlem  13948  seqeq3  13971  seqof  14024  ccatfval  14538  wrdl1s1  14579  ccat1st1st  14593  cshf1  14775  cshweqrep  14786  wrdlen2i  14908  wwlktovf  14922  wwlktovf1  14923  wwlktovfo  14924  wrd2f1tovbij  14926  rtrclreclem1  15023  dfrtrclrec2  15024  rtrclreclem2  15025  rtrclreclem4  15027  dfrtrcl2  15028  clim  15460  rlim  15461  ello1  15481  elo1  15492  summo  15683  fsum  15686  prodmo  15902  fprod  15907  bpolylem  16014  bpolyval  16015  vdwlem6  16957  vdwlem8  16959  ramcl  17000  strfvnd  17155  prdsplusgval  17436  prdsmulrval  17438  prdsleval  17440  prdsdsval  17441  prdsvscaval  17442  xpsff1o  17530  isacs2  17614  isnat  17912  yonedalem3b  18240  yonedainv  18242  ismgmhm  18623  ismhm  18712  prdspjmhm  18756  isgrpinv  18925  pwsmulg  19051  isghm  19147  isghmOLD  19148  cayleylem2  19343  symgfix2  19346  gsmsymgrfix  19358  gsmsymgreq  19362  symgfixelq  19363  pmtr3ncomlem2  19404  pmtrdifel  19410  pmtrdifwrdel  19415  pmtrdifwrdel2  19416  psgnunilem2  19425  psgnunilem3  19426  efgsdm  19660  efgredlemd  19674  efgredlem  19677  efgred  19678  efgrelexlema  19679  efgrelexlemb  19680  prdsgsum  19911  pwspjmhmmgpd  20237  pwsexpg  20238  isrnghm  20350  isabv  20720  islmhm  20934  frgpcyg  21483  psgndiflemB  21509  psgndiflemA  21510  dsmmelbas  21648  frlmipval  21688  frlmphl  21690  uvcf1  21701  islindf  21721  islindf4  21747  psrmulfval  21852  evlslem2  21986  evlslem3  21987  evlslem1  21989  mpfrcl  21992  selvval  22022  psdval  22046  psdcoef  22047  psdadd  22050  psdmul  22053  psdmvr  22056  coe1fval  22090  coe1mul2lem2  22154  coe1tm  22159  madetsumid  22348  mvmulval  22430  marepvval0  22453  mulmarep1gsum2  22461  mdetleib2  22475  m1detdiag  22484  mdetralt  22495  mdetunilem7  22505  mdetunilem9  22507  m2detleiblem3  22516  m2detleiblem4  22517  m2detleib  22518  symgmatr01lem  22540  gsummatr01lem1  22542  gsummatr01lem4  22545  gsummatr01  22546  smadiadetlem3  22555  pmatcoe1fsupp  22588  pmatcollpw3lem  22670  pmatcollpw3fi1lem2  22674  iscnp  23124  1stcfb  23332  ptpjpre1  23458  elpt  23459  elptr  23460  ptpjopn  23499  dfac14  23505  upxp  23510  pthaus  23525  ptrescn  23526  xkoptsub  23541  cnmptkp  23567  xkofvcn  23571  cnmptk1p  23572  cnmptk2  23573  ptunhmeo  23695  ptcmplem3  23941  ptcmplem4  23942  symgtgp  23993  prdstmdd  24011  isucn  24165  imasdsf1olem  24261  prdsxmslem2  24417  tngngp3  24544  nmoval  24603  elcncf  24782  ishtpy  24871  pcoval  24911  om1elbas  24932  elpi1i  24946  iscau  25176  rrxds  25293  rrxdsfival  25313  ehl1eudisval  25321  ehl2eudisval  25323  mbfi1fseqlem6  25621  mbfi1flimlem  25623  isibl  25666  deg1ldg  25997  deg1leb  26000  elply2  26101  elplyr  26106  ne0p  26112  coeeu  26130  coelem  26131  coeeq  26132  coeidlem  26142  elqaalem3  26229  qaa  26231  iaa  26233  aareccl  26234  aannenlem2  26237  aaliou2  26248  dchrptlem2  27176  dchrpt  27178  dchrsum2  27179  sumdchr2  27181  dchrvmaeq0  27415  rpvmasum2  27423  dchrisum0re  27424  ostth  27550  sltval  27559  nolesgn2o  27583  nogesgn1o  27585  noresle  27609  nosupprefixmo  27612  noinfprefixmo  27613  nosupcbv  27614  nosupfv  27618  noinfcbv  27629  noinffv  27633  iscgrg  28439  isismt  28461  israg  28624  iseqlg  28794  brbtwn  28826  brbtwn2  28832  colinearalg  28837  axsegconlem1  28844  axsegcon  28854  ax5seglem5  28860  axpasch  28868  axlowdim  28888  axeuclidlem  28889  axcontlem1  28891  axcontlem2  28892  axcontlem5  28895  vtxdgfval  29395  1egrvtxdg1  29437  isewlk  29530  iswlk  29538  uspgr2wlkeq2  29575  iswlkon  29585  isclwlk  29703  iscrct  29720  iscycl  29721  iswwlks  29766  wwlknon  29787  wlkiswwlks2  29805  wwlksnredwwlkn0  29826  wlksnwwlknvbij  29838  wwlksnextproplem3  29841  wwlksnextprop  29842  umgr2wlk  29879  midwwlks2s3  29882  elwwlks2  29896  elwspths2spth  29897  rusgrnumwwlkslem  29899  rusgrnumwwlkb0  29901  rusgrnumwwlks  29904  isclwwlk  29913  clwlkclwwlklem1  29928  clwwlkn1loopb  29972  clwwlkel  29975  clwwlkf  29976  clwwlkf1  29978  isclwwlknon  30020  clwwlknon1  30026  s2elclwwlknon2  30033  clwwlkvbij  30042  uhgr3cyclex  30111  fusgreg2wsplem  30262  fusgr2wsp2nb  30263  fusgreghash2wsp  30267  2clwwlkel  30278  extwwlkfabel  30282  numclwwlk1lem2fv  30285  numclwwlk1lem2  30289  clwwlknonclwlknonf1o  30291  dlwwlknondlwlknonf1o  30294  numclwwlk2lem1  30305  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  ex-fv  30372  isnvlem  30539  islno  30682  nmooval  30692  nmblolbi  30729  isphg  30746  ajmoi  30787  ajval  30790  ubthlem3  30801  htthlem  30846  hcau  31113  hlimi  31117  hosmval  31664  hommval  31665  hodmval  31666  hfsmval  31667  hfmmval  31668  adjmo  31761  nmopval  31785  elcnop  31786  ellnop  31787  elunop  31801  elhmop  31802  nmfnval  31805  elcnfn  31811  ellnfn  31812  adjeu  31818  adjval  31819  eigvecval  31825  eigvalfval  31826  adj1  31862  adjeq  31864  hmopadj2  31870  lnopeq0i  31936  lnopeq  31938  elunop2  31942  lnophm  31948  hmopco  31952  nmbdoplb  31954  nmcoplb  31959  lnopcon  31964  lnfn0  31976  lnfnmul  31977  nmbdfnlb  31979  nmcfnlb  31983  lnfncon  31985  riesz4  31993  riesz1  31994  cnlnadjlem9  32004  cnlnadjeu  32007  cnlnssadj  32009  nmopcoi  32024  bra11  32037  cnvbraval  32039  pjss2coi  32093  pjssdif2i  32103  pjssdif1i  32104  pjclem4  32128  pj3si  32136  pj3cor1i  32138  isst  32142  ishst  32143  stri  32186  hstri  32194  aciunf1lem  32586  ismnt  32909  mgcval  32913  ischn  32932  chnind  32937  chnub  32938  fzo0pmtrlast  33049  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  elrgspn  33197  elrgspnsubrunlem1  33198  linds2eq  33352  elrspunidl  33399  elrspunsn  33400  dfufd2lem  33520  lbsdiflsp0  33622  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  fldextrspunlsplem  33668  fldextrspunlsp  33669  fldext2chn  33718  constrextdg2lem  33738  constrextdg2  33739  lmatval  33803  mdetpmtr1  33813  zarcmplem  33871  ismeas  34189  isrnmeas  34190  cntnevol  34218  carsgval  34294  sitgval  34323  eulerpartleme  34354  eulerpartlemd  34357  eulerpartlemr  34365  eulerpartlemgvv  34367  eulerpart  34373  cndprobval  34424  signstfvneq0  34563  reprsum  34604  reprsuc  34606  reprpmtf1o  34617  reprdifc  34618  breprexp  34624  vtsval  34628  hgt750lemb  34647  hgt750lema  34648  hgt750leme  34649  bnj66  34850  bnj106  34858  bnj125  34862  bnj154  34868  bnj155  34869  bnj526  34878  bnj540  34882  bnj609  34907  bnj611  34908  bnj893  34918  bnj1000  34931  bnj1014  34951  bnj1015  34952  bnj1234  35003  bnj1463  35045  gblacfnacd  35089  loop1cycl  35124  derangenlem  35158  subfacp1lem3  35169  subfacp1lem5  35171  subfacp1lem6  35172  subfacp1  35173  sconnpht  35216  cnpconn  35217  txpconn  35219  ptpconn  35220  indispconn  35221  connpconn  35222  cvxpconn  35229  cvmliftmo  35271  cvmliftlem14  35284  cvmliftlem15  35285  cvmliftiota  35288  cvmlift2  35303  cvmliftphtlem  35304  cvmlift3lem2  35307  cvmlift3lem6  35311  cvmlift3lem7  35312  cvmlift3lem9  35314  cvmlift3  35315  satfv1lem  35349  satfv1  35350  sategoelfvb  35406  mrsubff1  35501  mrsub0  35503  mrsubccat  35505  mrsubcn  35506  elmsubrn  35515  msubrn  35516  msubco  35518  msubvrs  35547  mclsax  35556  shftvalg  35719  fwddifval  36150  fwddifnval  36151  bj-evalval  37063  unceq  37591  matunitlindflem2  37611  poimirlem17  37631  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem27  37641  poimirlem28  37642  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  poimir  37647  broucube  37648  voliunnfl  37658  volsupnfl  37659  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  ftc1anclem2  37688  ftc1anclem5  37691  upixp  37723  fdc  37739  isismty  37795  rrnmval  37822  elghomlem2OLD  37880  isrngohom  37959  islfl  39053  isopos  39173  islaut  40077  ispautN  40093  isldil  40104  isltrn  40113  ltrnid  40129  ltrneq2  40142  isdilN  40148  istrnN  40151  trlval  40156  ltrneq3  40202  cdleme50ex  40553  cdleme  40554  cdlemg1a  40564  ltrniotaval  40575  ltrniotavalbN  40578  cdlemeiota  40579  cdlemg2jlemOLDN  40587  cdlemg2fvlem  40588  cdlemg2klem  40589  istendo  40754  tendoplcbv  40769  tendopl  40770  tendoicbv  40787  tendoi  40788  tendoid0  40819  tendo1ne0  40822  cdlemksv2  40841  cdlemkuv2  40861  cdlemk33N  40903  cdlemk34  40904  cdlemk36  40907  cdlemk19u  40964  cdlemk  40968  tendoex  40969  dvavsca  41011  dvhvscacbv  41092  dvhvscaval  41093  dicopelval  41171  dicelval1sta  41181  diclspsn  41188  dihmeetlem13N  41313  dih1dimatlem0  41322  dih1dimatlem  41323  dihpN  41330  islpolN  41477  hdmap1fval  41790  hdmapfval  41821  sticksstones1  42134  sticksstones2  42135  sticksstones3  42136  sticksstones8  42141  sticksstones10  42143  sticksstones11  42144  sticksstones12a  42145  sticksstones12  42146  sticksstones15  42149  frlmsnic  42528  uvcn0  42530  pwsgprod  42532  mplmapghm  42544  evlsvval  42548  evlsvvval  42551  evlsvarval  42553  evlsbagval  42554  selvvvval  42573  evlselv  42575  fsuppssindlem2  42580  fsuppssind  42581  prjspnfv01  42612  prjspner01  42613  prjspner1  42614  sn-isghm  42661  ismrc  42689  mzpclval  42713  mzpsubst  42736  mzprename  42737  mzpcompact2lem  42739  eldioph  42746  eldioph2  42750  eldioph2b  42751  eldioph3  42754  rexrabdioph  42782  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  eldioph4i  42800  rabren3dioph  42803  mzpcong  42961  jm2.27dlem1  42998  wepwsolem  43031  aomclem6  43048  aomclem8  43050  dfac11  43051  dgraalem  43134  dgraaub  43137  dgraa0p  43138  mpaaeu  43139  mpaalem  43141  aaitgo  43151  rngunsnply  43158  cantnfresb  43313  tfsconcatun  43326  nvocnvb  43411  eliunov2  43668  rfovcnvfvd  43996  fsovfvd  43999  fsovcnvlem  44002  dssmapfv2d  44007  dssmapnvod  44009  clsk1independent  44035  ntrclskb  44058  ntrclsk13  44060  gneispace2  44121  mnringmulrvald  44216  dvconstbi  44323  addrval  44455  subrval  44456  mulvval  44457  relpeq1  44934  fnchoice  45023  refsum2cnlem1  45031  choicefi  45194  axccdom  45216  fmulcl  45579  fmuldfeqlem1  45580  mccllem  45595  mccl  45596  climf  45620  climf2  45664  dvnprodlem1  45944  dvnprodlem3  45946  dvnprod  45947  stoweidlem2  46000  stoweidlem6  46004  stoweidlem8  46006  stoweidlem9  46007  stoweidlem15  46013  stoweidlem16  46014  stoweidlem17  46015  stoweidlem18  46016  stoweidlem21  46019  stoweidlem27  46025  stoweidlem31  46029  stoweidlem36  46034  stoweidlem37  46035  stoweidlem41  46039  stoweidlem43  46041  stoweidlem44  46042  stoweidlem45  46043  stoweidlem46  46044  stoweidlem48  46046  stoweidlem51  46049  stoweidlem55  46053  stoweidlem59  46057  stoweidlem60  46058  stoweidlem62  46060  fourierdlem2  46107  fourierdlem3  46108  elaa2lem  46231  etransclem11  46243  etransclem24  46256  etransclem26  46258  etransclem28  46260  etransclem35  46267  rrndistlt  46288  ioorrnopn  46303  subsaliuncllem  46355  sge0val  46364  ismea  46449  caragenval  46491  isome  46492  isomenndlem  46528  hoicvrrex  46554  ovnlecvr  46556  ovncvrrp  46562  ovn0lem  46563  ovnsubaddlem1  46568  ovnsubadd  46570  hsphoif  46574  hoidmvval  46575  hsphoival  46577  hoidmvlelem3  46595  hoidmvlelem5  46597  hoidmvle  46598  ovnhoilem1  46599  ovnhoi  46601  ovnlecvr2  46608  ovncvr2  46609  hoidifhspval2  46613  hoiqssbllem2  46621  hspmbllem2  46625  hspmbllem3  46626  hspmbl  46627  ovnovollem1  46654  smfmullem2  46790  smfmul  46793  smfpimcclem  46805  tworepnotupword  46884  sinnpoly  46892  cfsetsnfsetfv  47058  cfsetsnfsetfo  47061  iccpart  47417  iccpartiun  47435  icceuelpart  47437  nnsum3primes4  47789  nnsum3primesgbe  47793  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbtbnd  47810  isisubgr  47862  isgrim  47882  grimidvtxedg  47885  grimcnv  47888  grimco  47889  isuspgrim0  47894  gricushgr  47917  ushggricedg  47927  uhgrimisgrgric  47931  isgrtri  47942  isubgr3stgrlem3  47967  isubgr3stgr  47974  isgrlim  47981  uspgrlim  47991  grlicref  48004  grlicsym  48005  grlictr  48007  isupwlk  48124  lincval  48398  lincdifsn  48413  linindslinci  48437  lindslinindsimp1  48446  linds0  48454  el0ldep  48455  lindsrng01  48457  snlindsntorlem  48459  ldepspr  48462  islindeps2  48472  zlmodzxzldep  48493  bigoval  48538  elbigo  48540  0aryfvalelfv  48624  1arympt1fv  48628  1arymaptfv  48629  1arymaptfo  48632  2arymptfv  48639  2arymaptfv  48640  2arymaptfo  48643  prelrrx2b  48703  rrx2plord  48709  rrx2vlinest  48730  rrx2linesl  48732  elrrx2linest2  48734  line2ylem  48740  line2xlem  48742  itsclc0  48760  itsclc0b  48761  itscnhlinecirc02p  48774  elfvne0  48837  iinfprg  49048  thincciso  49442  thinccisod  49443  setrecseq  49674  aacllem  49790