Theorem fveq1 6644

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 5032	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6308	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6332	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6332	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2858	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1538   class class class wbr 5030  ℩cio 6281  ‘cfv 6324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332

This theorem is referenced by:  fveq1i  6646  fveq1d  6647  iffv  6662  fvmptd3f  6760  fvmptdv2  6763  fsnex  7017  f1prex  7018  isoeq1  7049  oveq  7141  elovmpt3imp  7382  offval  7396  ofrfval  7397  offval3  7665  bropopvvv  7768  bropfvvvvlem  7769  wfrlem1  7937  wfrlem3a  7940  wfrlem15  7952  smoeq  7970  tfrlem12  8008  tz7.44-2  8026  tz7.44-3  8027  rdgeq1  8030  mapsncnv  8440  elixp2  8448  resixpfo  8483  elixpsn  8484  mapsnend  8571  enfixsn  8609  mapxpen  8667  ac6sfi  8746  ordtypelem7  8972  wemaplem1  8994  ixpiunwdom  9038  oemapval  9130  cantnf  9140  wemapwe  9144  cnfcom3clem  9152  updjud  9347  infxpenc2lem2  9431  fseqenlem1  9435  dfac8clem  9443  ac5num  9447  acni  9456  acni2  9457  acnlem  9459  dfac4  9533  dfac5lem5  9538  dfac2a  9540  dfac9  9547  dfacacn  9552  dfac12lem1  9554  dfac12r  9557  cofsmo  9680  cfsmolem  9681  cfsmo  9682  cfcoflem  9683  coftr  9684  alephsing  9687  isfin3ds  9740  fin23lem17  9749  fin23lem32  9755  fin23lem39  9761  isf33lem  9777  isf34lem6  9791  axcc2lem  9847  axcc3  9849  axdc2lem  9859  axdc3lem2  9862  axdc3lem3  9863  axdc3  9865  axdc4lem  9866  axcclem  9868  ac6num  9890  axdclem2  9931  konigthlem  9979  inar1  10186  1fv  13021  axdc4uzlem  13346  seqeq3  13369  seqof  13423  ccatfval  13916  wrdl1s1  13959  ccat1st1st  13975  cshf1  14163  cshweqrep  14174  wrdlen2i  14295  wwlktovf  14311  wwlktovf1  14312  wwlktovfo  14313  wrd2f1tovbij  14315  rtrclreclem1  14408  dfrtrclrec2  14409  rtrclreclem2  14410  rtrclreclem4  14412  dfrtrcl2  14413  clim  14843  rlim  14844  ello1  14864  elo1  14875  summo  15066  fsum  15069  prodmo  15282  fprod  15287  bpolylem  15394  bpolyval  15395  vdwlem6  16312  vdwlem8  16314  ramcl  16355  strfvnd  16494  prdsplusgval  16738  prdsmulrval  16740  prdsleval  16742  prdsdsval  16743  prdsvscaval  16744  xpsff1o  16832  isacs2  16916  isnat  17209  yonedalem3b  17521  yonedainv  17523  ismhm  17950  prdspjmhm  17985  isgrpinv  18148  pwsmulg  18264  isghm  18350  cayleylem2  18533  symgfix2  18536  gsmsymgrfix  18548  gsmsymgreq  18552  symgfixelq  18553  pmtr3ncomlem2  18594  pmtrdifel  18600  pmtrdifwrdel  18605  pmtrdifwrdel2  18606  psgnunilem2  18615  psgnunilem3  18616  efgsdm  18848  efgredlemd  18862  efgredlem  18865  efgred  18866  efgrelexlema  18867  efgrelexlemb  18868  prdsgsum  19094  isabv  19583  islmhm  19792  frgpcyg  20265  psgndiflemB  20289  psgndiflemA  20290  dsmmelbas  20428  frlmipval  20468  frlmphl  20470  uvcf1  20481  islindf  20501  islindf4  20527  psrmulfval  20623  evlslem2  20751  evlslem3  20752  evlslem1  20754  mpfrcl  20757  selvval  20790  coe1fval  20834  coe1mul2lem2  20897  coe1tm  20902  madetsumid  21066  mvmulval  21148  marepvval0  21171  mulmarep1gsum2  21179  mdetleib2  21193  m1detdiag  21202  mdetralt  21213  mdetunilem7  21223  mdetunilem9  21225  m2detleiblem3  21234  m2detleiblem4  21235  m2detleib  21236  symgmatr01lem  21258  gsummatr01lem1  21260  gsummatr01lem4  21263  gsummatr01  21264  smadiadetlem3  21273  pmatcoe1fsupp  21306  pmatcollpw3lem  21388  pmatcollpw3fi1lem2  21392  iscnp  21842  1stcfb  22050  ptpjpre1  22176  elpt  22177  elptr  22178  ptpjopn  22217  dfac14  22223  upxp  22228  pthaus  22243  ptrescn  22244  xkoptsub  22259  cnmptkp  22285  xkofvcn  22289  cnmptk1p  22290  cnmptk2  22291  ptunhmeo  22413  ptcmplem3  22659  ptcmplem4  22660  symgtgp  22711  prdstmdd  22729  isucn  22884  imasdsf1olem  22980  prdsxmslem2  23136  tngngp3  23262  nmoval  23321  elcncf  23494  ishtpy  23577  pcoval  23616  om1elbas  23637  elpi1i  23651  iscau  23880  rrxds  23997  rrxdsfival  24017  ehl1eudisval  24025  ehl2eudisval  24027  mbfi1fseqlem6  24324  mbfi1flimlem  24326  isibl  24369  deg1ldg  24693  deg1leb  24696  elply2  24793  elplyr  24798  ne0p  24804  coeeu  24822  coelem  24823  coeeq  24824  coeidlem  24834  elqaalem3  24917  qaa  24919  iaa  24921  aareccl  24922  aannenlem2  24925  aaliou2  24936  dchrptlem2  25849  dchrpt  25851  dchrsum2  25852  sumdchr2  25854  dchrvmaeq0  26088  rpvmasum2  26096  dchrisum0re  26097  ostth  26223  iscgrg  26306  isismt  26328  israg  26491  iseqlg  26661  brbtwn  26693  brbtwn2  26699  colinearalg  26704  axsegconlem1  26711  axsegcon  26721  ax5seglem5  26727  axpasch  26735  axlowdim  26755  axeuclidlem  26756  axcontlem1  26758  axcontlem2  26759  axcontlem5  26762  vtxdgfval  27257  1egrvtxdg1  27299  isewlk  27392  iswlk  27400  uspgr2wlkeq2  27436  iswlkon  27447  isclwlk  27562  iscrct  27579  iscycl  27580  iswwlks  27622  wwlknon  27643  wlkiswwlks2  27661  wwlksnredwwlkn0  27682  wlksnwwlknvbij  27694  wwlksnextproplem3  27697  wwlksnextprop  27698  umgr2wlk  27735  midwwlks2s3  27738  elwwlks2  27752  elwspths2spth  27753  rusgrnumwwlkslem  27755  rusgrnumwwlkb0  27757  rusgrnumwwlks  27760  isclwwlk  27769  clwlkclwwlklem1  27784  clwwlkn1loopb  27828  clwwlkel  27831  clwwlkf  27832  clwwlkf1  27834  isclwwlknon  27876  clwwlknon1  27882  s2elclwwlknon2  27889  clwwlkvbij  27898  uhgr3cyclex  27967  fusgreg2wsplem  28118  fusgr2wsp2nb  28119  fusgreghash2wsp  28123  2clwwlkel  28134  extwwlkfabel  28138  numclwwlk1lem2fv  28141  numclwwlk1lem2  28145  clwwlknonclwlknonf1o  28147  dlwwlknondlwlknonf1o  28150  numclwwlk2lem1  28161  numclwlk2lem2f  28162  numclwlk2lem2f1o  28164  ex-fv  28228  isnvlem  28393  islno  28536  nmooval  28546  nmblolbi  28583  isphg  28600  ajmoi  28641  ajval  28644  ubthlem3  28655  htthlem  28700  hcau  28967  hlimi  28971  hosmval  29518  hommval  29519  hodmval  29520  hfsmval  29521  hfmmval  29522  adjmo  29615  nmopval  29639  elcnop  29640  ellnop  29641  elunop  29655  elhmop  29656  nmfnval  29659  elcnfn  29665  ellnfn  29666  adjeu  29672  adjval  29673  eigvecval  29679  eigvalfval  29680  adj1  29716  adjeq  29718  hmopadj2  29724  lnopeq0i  29790  lnopeq  29792  elunop2  29796  lnophm  29802  hmopco  29806  nmbdoplb  29808  nmcoplb  29813  lnopcon  29818  lnfn0  29830  lnfnmul  29831  nmbdfnlb  29833  nmcfnlb  29837  lnfncon  29839  riesz4  29847  riesz1  29848  cnlnadjlem9  29858  cnlnadjeu  29861  cnlnssadj  29863  nmopcoi  29878  bra11  29891  cnvbraval  29893  pjss2coi  29947  pjssdif2i  29957  pjssdif1i  29958  pjclem4  29982  pj3si  29990  pj3cor1i  29992  isst  29996  ishst  29997  stri  30040  hstri  30048  aciunf1lem  30425  ismnt  30691  mgcval  30695  linds2eq  30995  elrspunidl  31014  lbsdiflsp0  31110  fedgmullem1  31113  fedgmullem2  31114  fedgmul  31115  lmatval  31166  mdetpmtr1  31176  zarcmplem  31234  ismeas  31568  isrnmeas  31569  cntnevol  31597  carsgval  31671  sitgval  31700  eulerpartleme  31731  eulerpartlemd  31734  eulerpartlemr  31742  eulerpartlemgvv  31744  eulerpart  31750  cndprobval  31801  signstfvneq0  31952  reprsum  31994  reprsuc  31996  reprpmtf1o  32007  reprdifc  32008  breprexp  32014  vtsval  32018  hgt750lemb  32037  hgt750lema  32038  hgt750leme  32039  bnj66  32242  bnj106  32250  bnj125  32254  bnj154  32260  bnj155  32261  bnj526  32270  bnj540  32274  bnj609  32299  bnj611  32300  bnj893  32310  bnj1000  32323  bnj1014  32343  bnj1015  32344  bnj1234  32395  bnj1463  32437  loop1cycl  32497  derangenlem  32531  subfacp1lem3  32542  subfacp1lem5  32544  subfacp1lem6  32545  subfacp1  32546  sconnpht  32589  cnpconn  32590  txpconn  32592  ptpconn  32593  indispconn  32594  connpconn  32595  cvxpconn  32602  cvmliftmo  32644  cvmliftlem14  32657  cvmliftlem15  32658  cvmliftiota  32661  cvmlift2  32676  cvmliftphtlem  32677  cvmlift3lem2  32680  cvmlift3lem6  32684  cvmlift3lem7  32685  cvmlift3lem9  32687  cvmlift3  32688  satfv1lem  32722  satfv1  32723  sategoelfvb  32779  mrsubff1  32874  mrsub0  32876  mrsubccat  32878  mrsubcn  32879  elmsubrn  32888  msubrn  32889  msubco  32891  msubvrs  32920  mclsax  32929  shftvalg  33076  poseq  33208  soseq  33209  frrlem1  33236  frrlem13  33248  sltval  33267  nolesgn2o  33291  noresle  33313  noprefixmo  33315  nosupfv  33319  fwddifval  33736  fwddifnval  33737  bj-evalval  34490  unceq  35034  matunitlindflem2  35054  poimirlem17  35074  poimirlem20  35077  poimirlem22  35079  poimirlem23  35080  poimirlem27  35084  poimirlem28  35085  poimirlem30  35087  poimirlem31  35088  poimirlem32  35089  poimir  35090  broucube  35091  voliunnfl  35101  volsupnfl  35102  itg2addnclem  35108  itg2addnclem3  35110  itg2addnc  35111  ftc1anclem2  35131  ftc1anclem5  35134  eqfnun  35160  upixp  35167  fdc  35183  isismty  35239  rrnmval  35266  elghomlem2OLD  35324  isrngohom  35403  islfl  36356  isopos  36476  islaut  37379  ispautN  37395  isldil  37406  isltrn  37415  ltrnid  37431  ltrneq2  37444  isdilN  37450  istrnN  37453  trlval  37458  ltrneq3  37504  cdleme50ex  37855  cdleme  37856  cdlemg1a  37866  ltrniotaval  37877  ltrniotavalbN  37880  cdlemeiota  37881  cdlemg2jlemOLDN  37889  cdlemg2fvlem  37890  cdlemg2klem  37891  istendo  38056  tendoplcbv  38071  tendopl  38072  tendoicbv  38089  tendoi  38090  tendoid0  38121  tendo1ne0  38124  cdlemksv2  38143  cdlemkuv2  38163  cdlemk33N  38205  cdlemk34  38206  cdlemk36  38209  cdlemk19u  38266  cdlemk  38270  tendoex  38271  dvavsca  38313  dvhvscacbv  38394  dvhvscaval  38395  dicopelval  38473  dicelval1sta  38483  diclspsn  38490  dihmeetlem13N  38615  dih1dimatlem0  38624  dih1dimatlem  38625  dihpN  38632  islpolN  38779  hdmap1fval  39092  hdmapfval  39123  frlmsnic  39453  uvcn0  39455  fsuppssindlem2  39458  fsuppssind  39459  ismrc  39642  mzpclval  39666  mzpsubst  39689  mzprename  39690  mzpcompact2lem  39692  eldioph  39699  eldioph2  39703  eldioph2b  39704  eldioph3  39707  rexrabdioph  39735  2rexfrabdioph  39737  3rexfrabdioph  39738  4rexfrabdioph  39739  6rexfrabdioph  39740  7rexfrabdioph  39741  eldioph4i  39753  rabren3dioph  39756  mzpcong  39913  jm2.27dlem1  39950  wepwsolem  39986  aomclem6  40003  aomclem8  40005  dfac11  40006  dgraalem  40089  dgraaub  40092  dgraa0p  40093  mpaaeu  40094  mpaalem  40096  aaitgo  40106  rngunsnply  40117  eliunov2  40380  rfovcnvfvd  40708  fsovfvd  40711  fsovcnvlem  40714  dssmapfv2d  40719  dssmapnvod  40721  clsk1independent  40749  ntrclskb  40772  ntrclsk13  40774  gneispace2  40835  mnringmulrvald  40935  dvconstbi  41038  addrval  41170  subrval  41171  mulvval  41172  fnchoice  41658  refsum2cnlem1  41666  choicefi  41829  axccdom  41853  fmulcl  42223  fmuldfeqlem1  42224  mccllem  42239  mccl  42240  climf  42264  climf2  42308  dvnprodlem1  42588  dvnprodlem3  42590  dvnprod  42591  stoweidlem2  42644  stoweidlem6  42648  stoweidlem8  42650  stoweidlem9  42651  stoweidlem15  42657  stoweidlem16  42658  stoweidlem17  42659  stoweidlem18  42660  stoweidlem21  42663  stoweidlem27  42669  stoweidlem31  42673  stoweidlem36  42678  stoweidlem37  42679  stoweidlem41  42683  stoweidlem43  42685  stoweidlem44  42686  stoweidlem45  42687  stoweidlem46  42688  stoweidlem48  42690  stoweidlem51  42693  stoweidlem55  42697  stoweidlem59  42701  stoweidlem60  42702  stoweidlem62  42704  fourierdlem2  42751  fourierdlem3  42752  elaa2lem  42875  etransclem11  42887  etransclem24  42900  etransclem26  42902  etransclem28  42904  etransclem35  42911  rrndistlt  42932  ioorrnopn  42947  subsaliuncllem  42997  sge0val  43005  ismea  43090  caragenval  43132  isome  43133  isomenndlem  43169  hoicvrrex  43195  ovnlecvr  43197  ovncvrrp  43203  ovn0lem  43204  ovnsubaddlem1  43209  ovnsubadd  43211  hsphoif  43215  hoidmvval  43216  hsphoival  43218  hoidmvlelem3  43236  hoidmvlelem5  43238  hoidmvle  43239  ovnhoilem1  43240  ovnhoi  43242  ovnlecvr2  43249  ovncvr2  43250  hoidifhspval2  43254  hoiqssbllem2  43262  hspmbllem2  43266  hspmbllem3  43267  hspmbl  43268  ovnovollem1  43295  smfmullem2  43424  smfmul  43427  smfpimcclem  43438  iccpart  43933  iccpartiun  43951  icceuelpart  43953  nnsum3primes4  44306  nnsum3primesgbe  44310  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbnd  44327  isomgreqve  44343  isomushgr  44344  isomuspgrlem2  44351  isomgrsym  44354  isomgrtr  44357  ushrisomgr  44359  isupwlk  44364  ismgmhm  44403  isrnghm  44516  lincval  44818  lincdifsn  44833  linindslinci  44857  lindslinindsimp1  44866  linds0  44874  el0ldep  44875  lindsrng01  44877  snlindsntorlem  44879  ldepspr  44882  islindeps2  44892  zlmodzxzldep  44913  bigoval  44963  elbigo  44965  0aryfvalelfv  45049  1arympt1fv  45053  1arymaptfv  45054  1arymaptfo  45057  2arymptfv  45064  2arymaptfv  45065  2arymaptfo  45068  prelrrx2b  45128  rrx2plord  45134  rrx2vlinest  45155  rrx2linesl  45157  elrrx2linest2  45159  line2ylem  45165  line2xlem  45167  itsclc0  45185  itsclc0b  45186  itscnhlinecirc02p  45199  setrecseq  45215  aacllem  45329