Theorem fveq1 6880

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

Syntax hints:   → wi 4   = wceq 1570   class class class wbr 5109  ℩cio 6490  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544

This theorem is referenced by:  fveq1i  6882  fveq1d  6883  iffv  6898  fvmptd3f  7005  fvmptdv2  7008  eqfnun  7032  fsnex  7281  f1prex  7282  isoeq1  7315  oveq  7416  elovmpt3imp  7667  ofrfvalg  7682  offval  7683  offval3  7975  bropopvvv  8081  bropfvvvvlem  8082  poseq  8150  soseq  8151  frrlem1  8279  frrlem13  8291  smoeq  8333  tfrlem12  8372  tz7.44-2  8390  tz7.44-3  8391  rdgeq1  8394  fsetfocdm  8854  fsetprcnex  8855  mapsncnv  8887  elixp2  8895  resixpfo  8930  elixpsn  8931  mapsnend  9029  enfixsn  9070  mapxpen  9127  ac6sfi  9240  ordtypelem7  9482  wemaplem1  9504  ixpiunwdom  9548  oemapval  9648  cantnf  9658  wemapwe  9662  cnfcom3clem  9670  ssttrcl  9680  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  updjud  9916  infxpenc2lem2  10000  fseqenlem1  10004  dfac8clem  10012  ac5num  10016  acni  10025  acni2  10026  acnlem  10028  dfac4  10102  dfac5lem5  10107  dfac2a  10109  dfac9  10116  dfacacn  10121  dfac12lem1  10123  dfac12r  10126  cofsmo  10248  cfsmolem  10249  cfsmo  10250  cfcoflem  10251  coftr  10252  alephsing  10255  isfin3ds  10308  fin23lem17  10317  fin23lem32  10323  fin23lem39  10329  isf33lem  10345  isf34lem6  10359  axcc2lem  10415  axcc3  10417  axdc2lem  10427  axdc3lem2  10430  axdc3lem3  10431  axdc3  10433  axdc4lem  10434  axcclem  10436  ac6num  10458  axdclem2  10499  konigthlem  10548  inar1  10755  1fv  13671  axdc4uzlem  14015  seqeq3  14038  seqof  14091  ccatfval  14606  wrdl1s1  14648  ccat1st1st  14662  cshf1  14843  cshweqrep  14854  wrdlen2i  14975  wwlktovf  14989  wwlktovf1  14990  wwlktovfo  14991  wrd2f1tovbij  14993  rtrclreclem1  15090  dfrtrclrec2  15091  rtrclreclem2  15092  rtrclreclem4  15094  dfrtrcl2  15095  clim  15541  rlim  15542  ello1  15562  elo1  15573  summo  15764  fsum  15767  prodmo  15986  fprod  15991  bpolylem  16097  bpolyval  16098  vdwlem6  17041  vdwlem8  17043  ramcl  17084  strfvnd  17240  prdsplusgval  17521  prdsmulrval  17523  prdsleval  17525  prdsdsval  17526  prdsvscaval  17527  xpsff1o  17616  isacs2  17704  isnat  18002  yonedalem3b  18330  yonedainv  18332  ischn  18658  chnind  18672  chnub  18673  ismgmhm  18749  ismhm  18838  prdspjmhm  18883  isgrpinv  19055  pwsmulg  19180  isghm  19281  cayleylem2  19478  symgfix2  19481  gsmsymgrfix  19493  gsmsymgreq  19497  symgfixelq  19498  pmtr3ncomlem2  19539  pmtrdifel  19545  pmtrdifwrdel  19550  pmtrdifwrdel2  19551  psgnunilem2  19560  psgnunilem3  19561  efgsdm  19795  efgredlemd  19809  efgredlem  19812  efgred  19813  efgrelexlema  19814  efgrelexlemb  19815  prdsgsum  20046  pwspjmhmmgpd  20405  pwsexpg  20406  pwsgprod  20407  isrnghm  20519  isrhm0  20554  isabv  20914  islmhm  21148  frgpcyg  21723  psgndiflemB  21750  psgndiflemA  21751  dsmmelbas  21889  frlmipval  21929  frlmphl  21931  uvcf1  21942  islindf  21962  islindf4  21988  psrmulfval  22093  evlslem2  22230  evlslem3  22231  evlslem1  22233  mpfrcl  22236  evlsvval  22241  evlsvvval  22244  selvval  22271  mplmapghm  22273  evlsvarval  22278  selvvvval  22293  psdval  22322  psdcoef  22323  psdadd  22326  psdmul  22329  psdmvr  22332  coe1fval  22365  coe1mul2lem2  22429  coe1tm  22434  madetsumid  22618  mvmulval  22700  marepvval0  22723  mulmarep1gsum2  22731  mdetleib2  22745  m1detdiag  22754  mdetralt  22765  mdetunilem7  22775  mdetunilem9  22777  m2detleiblem3  22786  m2detleiblem4  22787  m2detleib  22788  symgmatr01lem  22810  gsummatr01lem1  22812  gsummatr01lem4  22815  gsummatr01  22816  smadiadetlem3  22825  pmatcoe1fsupp  22858  pmatcollpw3lem  22940  pmatcollpw3fi1lem2  22944  iscnp  23394  1stcfb  23602  ptpjpre1  23728  elpt  23729  elptr  23730  ptpjopn  23769  dfac14  23775  upxp  23780  pthaus  23795  ptrescn  23796  xkoptsub  23811  cnmptkp  23837  xkofvcn  23841  cnmptk1p  23842  cnmptk2  23843  ptunhmeo  23965  ptcmplem3  24211  ptcmplem4  24212  symgtgp  24263  prdstmdd  24281  isucn  24434  imasdsf1olem  24530  prdsxmslem2  24686  tngngp3  24813  nmoval  24872  elcncf  25048  ishtpy  25131  pcoval  25170  om1elbas  25191  elpi1i  25205  iscau  25435  rrxds  25552  rrxdsfival  25572  ehl1eudisval  25580  ehl2eudisval  25582  mbfi1fseqlem6  25879  mbfi1flimlem  25881  isibl  25924  deg1ldg  26249  deg1leb  26252  elply2  26353  elplyr  26358  ne0p  26364  coeeu  26382  coelem  26383  coeeq  26384  coeidlem  26394  elqaalem3  26482  qaa  26484  iaa  26488  aareccl  26489  aannenlem2  26492  aaliou2  26503  dchrptlem2  27429  dchrpt  27431  dchrsum2  27432  sumdchr2  27434  dchrvmaeq0  27668  rpvmasum2  27676  dchrisum0re  27677  ostth  27803  ltsval  27811  nolesgn2o  27835  nogesgn1o  27837  noresle  27861  nosupprefixmo  27864  noinfprefixmo  27865  nosupcbv  27866  nosupfv  27870  noinfcbv  27881  noinffv  27885  iscgrg  28781  isismt  28803  israg  28977  iseqlg  29184  brbtwn  29249  brbtwn2  29255  colinearalg  29260  axsegconlem1  29267  axsegcon  29277  ax5seglem5  29283  axpasch  29291  axlowdim  29311  axeuclidlem  29312  axcontlem1  29314  axcontlem2  29315  axcontlem5  29318  vtxdgfval  29817  1egrvtxdg1  29859  isewlk  29952  iswlk  29960  uspgr2wlkeq2  29996  iswlkon  30005  isclwlk  30122  iscrct  30139  iscycl  30140  iswwlks  30185  wwlknon  30206  wlkiswwlks2  30224  wwlksnredwwlkn0  30245  wlksnwwlknvbij  30257  wwlksnextproplem3  30260  wwlksnextprop  30261  umgr2wlk  30298  midwwlks2s3  30301  elwwlks2  30318  elwspths2spth  30319  rusgrnumwwlkslem  30321  rusgrnumwwlkb0  30323  rusgrnumwwlks  30326  isclwwlk  30335  clwlkclwwlklem1  30350  clwwlkn1loopb  30394  clwwlkel  30397  clwwlkf  30398  clwwlkf1  30400  isclwwlknon  30442  clwwlknon1  30448  s2elclwwlknon2  30455  clwwlkvbij  30464  uhgr3cyclex  30533  fusgreg2wsplem  30684  fusgr2wsp2nb  30685  fusgreghash2wsp  30689  2clwwlkel  30700  extwwlkfabel  30704  numclwwlk1lem2fv  30707  numclwwlk1lem2  30711  clwwlknonclwlknonf1o  30713  dlwwlknondlwlknonf1o  30716  numclwwlk2lem1  30727  numclwlk2lem2f  30728  numclwlk2lem2f1o  30730  ex-fv  30794  isnvlem  30962  islno  31105  nmooval  31115  nmblolbi  31152  isphg  31169  ajmoi  31210  ajval  31213  ubthlem3  31224  htthlem  31269  hcau  31536  hlimi  31540  hosmval  32087  hommval  32088  hodmval  32089  hfsmval  32090  hfmmval  32091  adjmo  32184  nmopval  32208  elcnop  32209  ellnop  32210  elunop  32224  elhmop  32225  nmfnval  32228  elcnfn  32234  ellnfn  32235  adjeu  32241  adjval  32242  eigvecval  32248  eigvalfval  32249  adj1  32285  adjeq  32287  hmopadj2  32293  lnopeq0i  32359  lnopeq  32361  elunop2  32365  lnophm  32371  hmopco  32375  nmbdoplb  32377  nmcoplb  32382  lnopcon  32387  lnfn0  32399  lnfnmul  32400  nmbdfnlb  32402  nmcfnlb  32406  lnfncon  32408  riesz4  32416  riesz1  32417  cnlnadjlem9  32427  cnlnadjeu  32430  cnlnssadj  32432  nmopcoi  32447  bra11  32460  cnvbraval  32462  pjss2coi  32516  pjssdif2i  32526  pjssdif1i  32527  pjclem4  32551  pj3si  32559  pj3cor1i  32561  isst  32565  ishst  32566  stri  32609  hstri  32617  aciunf1lem  33007  ismnt  33303  mgcval  33307  fzo0pmtrlast  33412  elrgspnlem1  33562  elrgspnlem2  33563  elrgspnlem3  33564  elrgspnlem4  33565  elrgspn  33566  elrgspnsubrunlem1  33567  linds2eq  33694  elrspunidl  33736  elrspunsn  33737  dfufd2lem  33839  psrnzr  33902  0mplrim  33904  0mplric  33905  selvply1rhmlema  33908  selvply1rhmlemb  33909  selvply1rhmlem1  33910  selvply1rhmlem3  33912  selvply1rhmlem5  33914  selvply1rhm  33915  mplidom  33918  extvfv  33923  extvfvv  33924  extvfvcl  33926  evlvarval  33931  evlextv  33932  mplvrpmga  33935  splysubrg  33950  issply  33951  vietalem  33969  vieta  33970  lbsdiflsp0  34016  fedgmullem1  34019  fedgmullem2  34020  fedgmul  34021  fldextrspunlsplem  34063  fldextrspunlsp  34064  fldext2chn  34118  constrextdg2lem  34138  constrextdg2  34139  lmatval  34203  mdetpmtr1  34213  zarcmplem  34271  ismeas  34589  isrnmeas  34590  cntnevol  34618  carsgval  34693  sitgval  34722  eulerpartleme  34753  eulerpartlemd  34756  eulerpartlemr  34764  eulerpartlemgvv  34766  eulerpart  34772  cndprobval  34823  signstfvneq0  34959  reprsum  35000  reprsuc  35002  reprpmtf1o  35013  reprdifc  35014  breprexp  35020  vtsval  35024  hgt750lemb  35043  hgt750lema  35044  hgt750leme  35045  bnj66  35248  bnj106  35256  bnj125  35260  bnj154  35266  bnj155  35267  bnj526  35276  bnj540  35280  bnj609  35305  bnj611  35306  bnj893  35316  bnj1000  35329  bnj1014  35349  bnj1015  35350  bnj1234  35401  bnj1463  35443  fineqvnttrclse  35537  gblacfnacd  35586  loop1cycl  35629  derangenlem  35663  subfacp1lem3  35674  subfacp1lem5  35676  subfacp1lem6  35677  subfacp1  35678  sconnpht  35721  cnpconn  35722  txpconn  35724  ptpconn  35725  indispconn  35726  connpconn  35727  cvxpconn  35734  cvmliftmo  35776  cvmliftlem14  35789  cvmliftlem15  35790  cvmliftiota  35793  cvmlift2  35808  cvmliftphtlem  35809  cvmlift3lem2  35812  cvmlift3lem6  35816  cvmlift3lem7  35817  cvmlift3lem9  35819  cvmlift3  35820  satfv1lem  35854  satfv1  35855  sategoelfvb  35911  mrsubff1  36006  mrsub0  36008  mrsubccat  36010  mrsubcn  36011  elmsubrn  36020  msubrn  36021  msubco  36023  msubvrs  36052  mclsax  36061  shftvalg  36224  fwddifval  36654  fwddifnval  36655  bj-evalval  37717  unceq  38248  matunitlindflem2  38268  poimirlem17  38288  poimirlem20  38291  poimirlem22  38293  poimirlem23  38294  poimirlem27  38298  poimirlem28  38299  poimirlem30  38301  poimirlem31  38302  poimirlem32  38303  poimir  38304  broucube  38305  voliunnfl  38315  volsupnfl  38316  itg2addnclem  38322  itg2addnclem3  38324  itg2addnc  38325  ftc1anclem2  38345  ftc1anclem5  38348  upixp  38380  fdc  38396  isismty  38452  rrnmval  38479  elghomlem2OLD  38537  isrngohom  38616  islfl  39834  isopos  39954  islaut  40857  ispautN  40873  isldil  40884  isltrn  40893  ltrnid  40909  ltrneq2  40922  isdilN  40928  istrnN  40931  trlval  40936  ltrneq3  40982  cdleme50ex  41333  cdleme  41334  cdlemg1a  41344  ltrniotaval  41355  ltrniotavalbN  41358  cdlemeiota  41359  cdlemg2jlemOLDN  41367  cdlemg2fvlem  41368  cdlemg2klem  41369  istendo  41534  tendoplcbv  41549  tendopl  41550  tendoicbv  41567  tendoi  41568  tendoid0  41599  tendo1ne0  41602  cdlemksv2  41621  cdlemkuv2  41641  cdlemk33N  41683  cdlemk34  41684  cdlemk36  41687  cdlemk19u  41744  cdlemk  41748  tendoex  41749  dvavsca  41791  dvhvscacbv  41872  dvhvscaval  41873  dicopelval  41951  dicelval1sta  41961  diclspsn  41968  dihmeetlem13N  42093  dih1dimatlem0  42102  dih1dimatlem  42103  dihpN  42110  islpolN  42257  hdmap1fval  42570  hdmapfval  42601  sticksstones1  42913  sticksstones2  42914  sticksstones3  42915  sticksstones8  42920  sticksstones10  42922  sticksstones11  42923  sticksstones12a  42924  sticksstones12  42925  sticksstones15  42928  frlmsnic  43308  uvcn0  43310  evlsbagval  43318  evlselv  43321  fsuppssindlem2  43324  fsuppssind  43325  prjspnfv01  43356  prjspner01  43357  prjspner1  43358  sn-isghm  43405  ismrc  43432  mzpclval  43456  mzpsubst  43479  mzprename  43480  mzpcompact2lem  43482  eldioph  43489  eldioph2  43493  eldioph2b  43494  eldioph3  43497  rexrabdioph  43521  2rexfrabdioph  43523  3rexfrabdioph  43524  4rexfrabdioph  43525  6rexfrabdioph  43526  7rexfrabdioph  43527  eldioph4i  43539  rabren3dioph  43542  mzpcong  43699  jm2.27dlem1  43736  wepwsolem  43769  aomclem6  43786  aomclem8  43788  dfac11  43789  dgraalem  43872  dgraaub  43875  dgraa0p  43876  mpaaeu  43877  mpaalem  43879  aaitgo  43889  rngunsnply  43896  cantnfresb  44051  tfsconcatun  44064  nvocnvb  44148  eliunov2  44405  rfovcnvfvd  44733  fsovfvd  44736  fsovcnvlem  44739  dssmapfv2d  44744  dssmapnvod  44746  clsk1independent  44772  ntrclskb  44795  ntrclsk13  44797  gneispace2  44858  mnringmulrvald  44951  dvconstbi  45044  addrval  45174  subrval  45175  mulvval  45176  relpeq1  45653  fnchoice  45749  refsum2cnlem1  45757  choicefi  45917  axccdom  45938  fmulcl  46297  fmuldfeqlem1  46298  mccllem  46313  mccl  46314  climf  46338  climf2  46380  dvnprodlem1  46660  dvnprodlem3  46662  dvnprod  46663  stoweidlem2  46716  stoweidlem6  46720  stoweidlem8  46722  stoweidlem9  46723  stoweidlem15  46729  stoweidlem16  46730  stoweidlem17  46731  stoweidlem18  46732  stoweidlem21  46735  stoweidlem27  46741  stoweidlem31  46745  stoweidlem36  46750  stoweidlem37  46751  stoweidlem41  46755  stoweidlem43  46757  stoweidlem44  46758  stoweidlem45  46759  stoweidlem46  46760  stoweidlem48  46762  stoweidlem51  46765  stoweidlem55  46769  stoweidlem59  46773  stoweidlem60  46774  stoweidlem62  46776  fourierdlem2  46823  fourierdlem3  46824  elaa2lem  46947  etransclem11  46959  etransclem24  46972  etransclem26  46974  etransclem28  46976  etransclem35  46983  rrndistlt  47004  ioorrnopn  47019  subsaliuncllem  47071  sge0val  47080  ismea  47165  caragenval  47207  isome  47208  isomenndlem  47244  hoicvrrex  47270  ovnlecvr  47272  ovncvrrp  47278  ovn0lem  47279  ovnsubaddlem1  47284  ovnsubadd  47286  hsphoif  47290  hoidmvval  47291  hsphoival  47293  hoidmvlelem3  47311  hoidmvlelem5  47313  hoidmvle  47314  ovnhoilem1  47315  ovnhoi  47317  ovnlecvr2  47324  ovncvr2  47325  hoidifhspval2  47329  hoiqssbllem2  47337  hspmbllem2  47341  hspmbllem3  47342  hspmbl  47343  ovnovollem1  47370  smfmullem2  47506  smfmul  47509  smfpimcclem  47521  chnerlem1  47598  sqrtnnaa  47604  sqrtnzqaa  47605  sinnpoly  47628  cfsetsnfsetfv  47794  cfsetsnfsetfo  47797  iccpart  48165  iccpartiun  48183  icceuelpart  48185  nnsum3primes4  48553  nnsum3primesgbe  48557  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  bgoldbtbnd  48574  isisubgr  48627  isgrim  48647  grimidvtxedg  48650  grimcnv  48653  grimco  48654  isuspgrim0  48659  gricushgr  48682  ushggricedg  48692  uhgrimisgrgric  48696  isgrtri  48708  isubgr3stgrlem3  48733  isubgr3stgr  48740  isgrlim  48747  uspgrlim  48757  grlicref  48777  grlicsym  48778  grlictr  48780  grlimedgnedg  48896  isupwlk  48901  lincval  49189  lincdifsn  49204  linindslinci  49228  lindslinindsimp1  49237  linds0  49245  el0ldep  49246  lindsrng01  49248  snlindsntorlem  49250  ldepspr  49253  islindeps2  49263  zlmodzxzldep  49284  bigoval  49329  elbigo  49331  0aryfvalelfv  49415  1arympt1fv  49419  1arymaptfv  49420  1arymaptfo  49423  2arymptfv  49430  2arymaptfv  49431  2arymaptfo  49434  prelrrx2b  49494  rrx2plord  49500  rrx2vlinest  49521  rrx2linesl  49523  elrrx2linest2  49525  line2ylem  49531  line2xlem  49533  itsclc0  49551  itsclc0b  49552  itscnhlinecirc02p  49565  elfvne0  49627  iinfprg  49837  thincciso  50231  thinccisod  50232  setrecseq  50463  aacllem  50621