Theorem fveq1 6782

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 5077	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6421	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6445	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6445	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2804	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5075  ℩cio 6393  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445

This theorem is referenced by:  fveq1i  6784  fveq1d  6785  iffv  6800  fvmptd3f  6899  fvmptdv2  6902  fsnex  7164  f1prex  7165  isoeq1  7197  oveq  7290  elovmpt3imp  7535  ofrfvalg  7550  offval  7551  offval3  7834  bropopvvv  7939  bropfvvvvlem  7940  frrlem1  8111  frrlem13  8123  wfrlem1OLD  8148  wfrlem3OLDa  8151  wfrlem15OLD  8163  smoeq  8190  tfrlem12  8229  tz7.44-2  8247  tz7.44-3  8248  rdgeq1  8251  fsetfocdm  8658  fsetprcnex  8659  mapsncnv  8690  elixp2  8698  resixpfo  8733  elixpsn  8734  mapsnend  8835  enfixsn  8877  mapxpen  8939  ac6sfi  9067  ordtypelem7  9292  wemaplem1  9314  ixpiunwdom  9358  oemapval  9450  cantnf  9460  wemapwe  9464  cnfcom3clem  9472  ssttrcl  9482  ttrcltr  9483  ttrclss  9487  ttrclselem2  9493  updjud  9701  infxpenc2lem2  9785  fseqenlem1  9789  dfac8clem  9797  ac5num  9801  acni  9810  acni2  9811  acnlem  9813  dfac4  9887  dfac5lem5  9892  dfac2a  9894  dfac9  9901  dfacacn  9906  dfac12lem1  9908  dfac12r  9911  cofsmo  10034  cfsmolem  10035  cfsmo  10036  cfcoflem  10037  coftr  10038  alephsing  10041  isfin3ds  10094  fin23lem17  10103  fin23lem32  10109  fin23lem39  10115  isf33lem  10131  isf34lem6  10145  axcc2lem  10201  axcc3  10203  axdc2lem  10213  axdc3lem2  10216  axdc3lem3  10217  axdc3  10219  axdc4lem  10220  axcclem  10222  ac6num  10244  axdclem2  10285  konigthlem  10333  inar1  10540  1fv  13384  axdc4uzlem  13712  seqeq3  13735  seqof  13789  ccatfval  14285  wrdl1s1  14328  ccat1st1st  14344  cshf1  14532  cshweqrep  14543  wrdlen2i  14664  wwlktovf  14680  wwlktovf1  14681  wwlktovfo  14682  wrd2f1tovbij  14684  rtrclreclem1  14777  dfrtrclrec2  14778  rtrclreclem2  14779  rtrclreclem4  14781  dfrtrcl2  14782  clim  15212  rlim  15213  ello1  15233  elo1  15244  summo  15438  fsum  15441  prodmo  15655  fprod  15660  bpolylem  15767  bpolyval  15768  vdwlem6  16696  vdwlem8  16698  ramcl  16739  strfvnd  16895  prdsplusgval  17193  prdsmulrval  17195  prdsleval  17197  prdsdsval  17198  prdsvscaval  17199  xpsff1o  17287  isacs2  17371  isnat  17672  yonedalem3b  18006  yonedainv  18008  ismhm  18441  prdspjmhm  18476  isgrpinv  18641  pwsmulg  18757  isghm  18843  cayleylem2  19030  symgfix2  19033  gsmsymgrfix  19045  gsmsymgreq  19049  symgfixelq  19050  pmtr3ncomlem2  19091  pmtrdifel  19097  pmtrdifwrdel  19102  pmtrdifwrdel2  19103  psgnunilem2  19112  psgnunilem3  19113  efgsdm  19345  efgredlemd  19359  efgredlem  19362  efgred  19363  efgrelexlema  19364  efgrelexlemb  19365  prdsgsum  19591  isabv  20088  islmhm  20298  frgpcyg  20790  psgndiflemB  20814  psgndiflemA  20815  dsmmelbas  20955  frlmipval  20995  frlmphl  20997  uvcf1  21008  islindf  21028  islindf4  21054  psrmulfval  21163  evlslem2  21298  evlslem3  21299  evlslem1  21301  mpfrcl  21304  selvval  21337  coe1fval  21385  coe1mul2lem2  21448  coe1tm  21453  madetsumid  21619  mvmulval  21701  marepvval0  21724  mulmarep1gsum2  21732  mdetleib2  21746  m1detdiag  21755  mdetralt  21766  mdetunilem7  21776  mdetunilem9  21778  m2detleiblem3  21787  m2detleiblem4  21788  m2detleib  21789  symgmatr01lem  21811  gsummatr01lem1  21813  gsummatr01lem4  21816  gsummatr01  21817  smadiadetlem3  21826  pmatcoe1fsupp  21859  pmatcollpw3lem  21941  pmatcollpw3fi1lem2  21945  iscnp  22397  1stcfb  22605  ptpjpre1  22731  elpt  22732  elptr  22733  ptpjopn  22772  dfac14  22778  upxp  22783  pthaus  22798  ptrescn  22799  xkoptsub  22814  cnmptkp  22840  xkofvcn  22844  cnmptk1p  22845  cnmptk2  22846  ptunhmeo  22968  ptcmplem3  23214  ptcmplem4  23215  symgtgp  23266  prdstmdd  23284  isucn  23439  imasdsf1olem  23535  prdsxmslem2  23694  tngngp3  23829  nmoval  23888  elcncf  24061  ishtpy  24144  pcoval  24183  om1elbas  24204  elpi1i  24218  iscau  24449  rrxds  24566  rrxdsfival  24586  ehl1eudisval  24594  ehl2eudisval  24596  mbfi1fseqlem6  24894  mbfi1flimlem  24896  isibl  24939  deg1ldg  25266  deg1leb  25269  elply2  25366  elplyr  25371  ne0p  25377  coeeu  25395  coelem  25396  coeeq  25397  coeidlem  25407  elqaalem3  25490  qaa  25492  iaa  25494  aareccl  25495  aannenlem2  25498  aaliou2  25509  dchrptlem2  26422  dchrpt  26424  dchrsum2  26425  sumdchr2  26427  dchrvmaeq0  26661  rpvmasum2  26669  dchrisum0re  26670  ostth  26796  iscgrg  26882  isismt  26904  israg  27067  iseqlg  27237  brbtwn  27276  brbtwn2  27282  colinearalg  27287  axsegconlem1  27294  axsegcon  27304  ax5seglem5  27310  axpasch  27318  axlowdim  27338  axeuclidlem  27339  axcontlem1  27341  axcontlem2  27342  axcontlem5  27345  vtxdgfval  27843  1egrvtxdg1  27885  isewlk  27978  iswlk  27986  uspgr2wlkeq2  28023  iswlkon  28034  isclwlk  28150  iscrct  28167  iscycl  28168  iswwlks  28210  wwlknon  28231  wlkiswwlks2  28249  wwlksnredwwlkn0  28270  wlksnwwlknvbij  28282  wwlksnextproplem3  28285  wwlksnextprop  28286  umgr2wlk  28323  midwwlks2s3  28326  elwwlks2  28340  elwspths2spth  28341  rusgrnumwwlkslem  28343  rusgrnumwwlkb0  28345  rusgrnumwwlks  28348  isclwwlk  28357  clwlkclwwlklem1  28372  clwwlkn1loopb  28416  clwwlkel  28419  clwwlkf  28420  clwwlkf1  28422  isclwwlknon  28464  clwwlknon1  28470  s2elclwwlknon2  28477  clwwlkvbij  28486  uhgr3cyclex  28555  fusgreg2wsplem  28706  fusgr2wsp2nb  28707  fusgreghash2wsp  28711  2clwwlkel  28722  extwwlkfabel  28726  numclwwlk1lem2fv  28729  numclwwlk1lem2  28733  clwwlknonclwlknonf1o  28735  dlwwlknondlwlknonf1o  28738  numclwwlk2lem1  28749  numclwlk2lem2f  28750  numclwlk2lem2f1o  28752  ex-fv  28816  isnvlem  28981  islno  29124  nmooval  29134  nmblolbi  29171  isphg  29188  ajmoi  29229  ajval  29232  ubthlem3  29243  htthlem  29288  hcau  29555  hlimi  29559  hosmval  30106  hommval  30107  hodmval  30108  hfsmval  30109  hfmmval  30110  adjmo  30203  nmopval  30227  elcnop  30228  ellnop  30229  elunop  30243  elhmop  30244  nmfnval  30247  elcnfn  30253  ellnfn  30254  adjeu  30260  adjval  30261  eigvecval  30267  eigvalfval  30268  adj1  30304  adjeq  30306  hmopadj2  30312  lnopeq0i  30378  lnopeq  30380  elunop2  30384  lnophm  30390  hmopco  30394  nmbdoplb  30396  nmcoplb  30401  lnopcon  30406  lnfn0  30418  lnfnmul  30419  nmbdfnlb  30421  nmcfnlb  30425  lnfncon  30427  riesz4  30435  riesz1  30436  cnlnadjlem9  30446  cnlnadjeu  30449  cnlnssadj  30451  nmopcoi  30466  bra11  30479  cnvbraval  30481  pjss2coi  30535  pjssdif2i  30545  pjssdif1i  30546  pjclem4  30570  pj3si  30578  pj3cor1i  30580  isst  30584  ishst  30585  stri  30628  hstri  30636  aciunf1lem  31008  ismnt  31270  mgcval  31274  linds2eq  31584  elrspunidl  31615  lbsdiflsp0  31716  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  lmatval  31772  mdetpmtr1  31782  zarcmplem  31840  ismeas  32176  isrnmeas  32177  cntnevol  32205  carsgval  32279  sitgval  32308  eulerpartleme  32339  eulerpartlemd  32342  eulerpartlemr  32350  eulerpartlemgvv  32352  eulerpart  32358  cndprobval  32409  signstfvneq0  32560  reprsum  32602  reprsuc  32604  reprpmtf1o  32615  reprdifc  32616  breprexp  32622  vtsval  32626  hgt750lemb  32645  hgt750lema  32646  hgt750leme  32647  bnj66  32849  bnj106  32857  bnj125  32861  bnj154  32867  bnj155  32868  bnj526  32877  bnj540  32881  bnj609  32906  bnj611  32907  bnj893  32917  bnj1000  32930  bnj1014  32950  bnj1015  32951  bnj1234  33002  bnj1463  33044  loop1cycl  33108  derangenlem  33142  subfacp1lem3  33153  subfacp1lem5  33155  subfacp1lem6  33156  subfacp1  33157  sconnpht  33200  cnpconn  33201  txpconn  33203  ptpconn  33204  indispconn  33205  connpconn  33206  cvxpconn  33213  cvmliftmo  33255  cvmliftlem14  33268  cvmliftlem15  33269  cvmliftiota  33272  cvmlift2  33287  cvmliftphtlem  33288  cvmlift3lem2  33291  cvmlift3lem6  33295  cvmlift3lem7  33296  cvmlift3lem9  33298  cvmlift3  33299  satfv1lem  33333  satfv1  33334  sategoelfvb  33390  mrsubff1  33485  mrsub0  33487  mrsubccat  33489  mrsubcn  33490  elmsubrn  33499  msubrn  33500  msubco  33502  msubvrs  33531  mclsax  33540  shftvalg  33706  poseq  33811  soseq  33812  sltval  33859  nolesgn2o  33883  nogesgn1o  33885  noresle  33909  nosupprefixmo  33912  noinfprefixmo  33913  nosupcbv  33914  nosupfv  33918  noinfcbv  33929  noinffv  33933  fwddifval  34473  fwddifnval  34474  bj-evalval  35255  unceq  35763  matunitlindflem2  35783  poimirlem17  35803  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimirlem27  35813  poimirlem28  35814  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  poimir  35819  broucube  35820  voliunnfl  35830  volsupnfl  35831  itg2addnclem  35837  itg2addnclem3  35839  itg2addnc  35840  ftc1anclem2  35860  ftc1anclem5  35863  eqfnun  35889  upixp  35896  fdc  35912  isismty  35968  rrnmval  35995  elghomlem2OLD  36053  isrngohom  36132  islfl  37081  isopos  37201  islaut  38104  ispautN  38120  isldil  38131  isltrn  38140  ltrnid  38156  ltrneq2  38169  isdilN  38175  istrnN  38178  trlval  38183  ltrneq3  38229  cdleme50ex  38580  cdleme  38581  cdlemg1a  38591  ltrniotaval  38602  ltrniotavalbN  38605  cdlemeiota  38606  cdlemg2jlemOLDN  38614  cdlemg2fvlem  38615  cdlemg2klem  38616  istendo  38781  tendoplcbv  38796  tendopl  38797  tendoicbv  38814  tendoi  38815  tendoid0  38846  tendo1ne0  38849  cdlemksv2  38868  cdlemkuv2  38888  cdlemk33N  38930  cdlemk34  38931  cdlemk36  38934  cdlemk19u  38991  cdlemk  38995  tendoex  38996  dvavsca  39038  dvhvscacbv  39119  dvhvscaval  39120  dicopelval  39198  dicelval1sta  39208  diclspsn  39215  dihmeetlem13N  39340  dih1dimatlem0  39349  dih1dimatlem  39350  dihpN  39357  islpolN  39504  hdmap1fval  39817  hdmapfval  39848  sticksstones1  40109  sticksstones2  40110  sticksstones3  40111  sticksstones8  40116  sticksstones10  40118  sticksstones11  40119  sticksstones12a  40120  sticksstones12  40121  sticksstones15  40124  frlmsnic  40270  uvcn0  40272  pwspjmhmmgpd  40274  pwsexpg  40275  pwsgprod  40276  evlsvarval  40281  evlsbagval  40282  fsuppssindlem2  40288  fsuppssind  40289  prjspnfv01  40468  prjspner01  40469  prjspner1  40470  ismrc  40530  mzpclval  40554  mzpsubst  40577  mzprename  40578  mzpcompact2lem  40580  eldioph  40587  eldioph2  40591  eldioph2b  40592  eldioph3  40595  rexrabdioph  40623  2rexfrabdioph  40625  3rexfrabdioph  40626  4rexfrabdioph  40627  6rexfrabdioph  40628  7rexfrabdioph  40629  eldioph4i  40641  rabren3dioph  40644  mzpcong  40801  jm2.27dlem1  40838  wepwsolem  40874  aomclem6  40891  aomclem8  40893  dfac11  40894  dgraalem  40977  dgraaub  40980  dgraa0p  40981  mpaaeu  40982  mpaalem  40984  aaitgo  40994  rngunsnply  41005  eliunov2  41294  rfovcnvfvd  41622  fsovfvd  41625  fsovcnvlem  41628  dssmapfv2d  41633  dssmapnvod  41635  clsk1independent  41663  ntrclskb  41686  ntrclsk13  41688  gneispace2  41749  mnringmulrvald  41852  dvconstbi  41959  addrval  42091  subrval  42092  mulvval  42093  fnchoice  42579  refsum2cnlem1  42587  choicefi  42747  axccdom  42769  fmulcl  43129  fmuldfeqlem1  43130  mccllem  43145  mccl  43146  climf  43170  climf2  43214  dvnprodlem1  43494  dvnprodlem3  43496  dvnprod  43497  stoweidlem2  43550  stoweidlem6  43554  stoweidlem8  43556  stoweidlem9  43557  stoweidlem15  43563  stoweidlem16  43564  stoweidlem17  43565  stoweidlem18  43566  stoweidlem21  43569  stoweidlem27  43575  stoweidlem31  43579  stoweidlem36  43584  stoweidlem37  43585  stoweidlem41  43589  stoweidlem43  43591  stoweidlem44  43592  stoweidlem45  43593  stoweidlem46  43594  stoweidlem48  43596  stoweidlem51  43599  stoweidlem55  43603  stoweidlem59  43607  stoweidlem60  43608  stoweidlem62  43610  fourierdlem2  43657  fourierdlem3  43658  elaa2lem  43781  etransclem11  43793  etransclem24  43806  etransclem26  43808  etransclem28  43810  etransclem35  43817  rrndistlt  43838  ioorrnopn  43853  subsaliuncllem  43903  sge0val  43911  ismea  43996  caragenval  44038  isome  44039  isomenndlem  44075  hoicvrrex  44101  ovnlecvr  44103  ovncvrrp  44109  ovn0lem  44110  ovnsubaddlem1  44115  ovnsubadd  44117  hsphoif  44121  hoidmvval  44122  hsphoival  44124  hoidmvlelem3  44142  hoidmvlelem5  44144  hoidmvle  44145  ovnhoilem1  44146  ovnhoi  44148  ovnlecvr2  44155  ovncvr2  44156  hoidifhspval2  44160  hoiqssbllem2  44168  hspmbllem2  44172  hspmbllem3  44173  hspmbl  44174  ovnovollem1  44201  smfmullem2  44337  smfmul  44340  smfpimcclem  44351  cfsetsnfsetfv  44562  cfsetsnfsetfo  44565  iccpart  44879  iccpartiun  44897  icceuelpart  44899  nnsum3primes4  45251  nnsum3primesgbe  45255  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  bgoldbtbnd  45272  isomgreqve  45288  isomushgr  45289  isomuspgrlem2  45296  isomgrsym  45299  isomgrtr  45302  ushrisomgr  45304  isupwlk  45309  ismgmhm  45348  isrnghm  45461  lincval  45761  lincdifsn  45776  linindslinci  45800  lindslinindsimp1  45809  linds0  45817  el0ldep  45818  lindsrng01  45820  snlindsntorlem  45822  ldepspr  45825  islindeps2  45835  zlmodzxzldep  45856  bigoval  45906  elbigo  45908  0aryfvalelfv  45992  1arympt1fv  45996  1arymaptfv  45997  1arymaptfo  46000  2arymptfv  46007  2arymaptfv  46008  2arymaptfo  46011  prelrrx2b  46071  rrx2plord  46077  rrx2vlinest  46098  rrx2linesl  46100  elrrx2linest2  46102  line2ylem  46108  line2xlem  46110  itsclc0  46128  itsclc0b  46129  itscnhlinecirc02p  46142  elfvne0  46187  thincciso  46341  setrecseq  46402  aacllem  46516  tworepnotupword  46532