Theorem fveq1 6669

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 5068	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6339	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6363	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6363	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2881	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5066  ℩cio 6312  ‘cfv 6355

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363

This theorem is referenced by:  fveq1i  6671  fveq1d  6672  iffv  6687  fvmptd3f  6783  fvmptdv2  6786  fsnex  7039  f1prex  7040  isoeq1  7070  oveq  7162  elovmpt3imp  7402  offval  7416  ofrfval  7417  offval3  7683  bropopvvv  7785  bropfvvvvlem  7786  wfrlem1  7954  wfrlem3a  7957  wfrlem15  7969  smoeq  7987  tfrlem12  8025  tz7.44-2  8043  tz7.44-3  8044  rdgeq1  8047  mapsncnv  8457  elixp2  8465  resixpfo  8500  elixpsn  8501  mapsnend  8588  enfixsn  8626  mapxpen  8683  ac6sfi  8762  ordtypelem7  8988  wemaplem1  9010  ixpiunwdom  9055  oemapval  9146  cantnf  9156  wemapwe  9160  cnfcom3clem  9168  updjud  9363  infxpenc2lem2  9446  fseqenlem1  9450  dfac8clem  9458  ac5num  9462  acni  9471  acni2  9472  acnlem  9474  dfac4  9548  dfac5lem5  9553  dfac2a  9555  dfac9  9562  dfacacn  9567  dfac12lem1  9569  dfac12r  9572  cofsmo  9691  cfsmolem  9692  cfsmo  9693  cfcoflem  9694  coftr  9695  alephsing  9698  isfin3ds  9751  fin23lem17  9760  fin23lem32  9766  fin23lem39  9772  isf33lem  9788  isf34lem6  9802  axcc2lem  9858  axcc3  9860  axdc2lem  9870  axdc3lem2  9873  axdc3lem3  9874  axdc3  9876  axdc4lem  9877  axcclem  9879  ac6num  9901  axdclem2  9942  konigthlem  9990  inar1  10197  1fv  13027  axdc4uzlem  13352  seqeq3  13375  seqof  13428  ccatfval  13925  wrdl1s1  13968  ccat1st1st  13984  cshf1  14172  cshweqrep  14183  wrdlen2i  14304  wwlktovf  14320  wwlktovf1  14321  wwlktovfo  14322  wrd2f1tovbij  14324  dfrtrclrec2  14416  rtrclreclem1  14417  rtrclreclem2  14418  rtrclreclem4  14420  dfrtrcl2  14421  clim  14851  rlim  14852  ello1  14872  elo1  14883  summo  15074  fsum  15077  prodmo  15290  fprod  15295  bpolylem  15402  bpolyval  15403  vdwlem6  16322  vdwlem8  16324  ramcl  16365  strfvnd  16502  prdsplusgval  16746  prdsmulrval  16748  prdsleval  16750  prdsdsval  16751  prdsvscaval  16752  xpsff1o  16840  isacs2  16924  isnat  17217  yonedalem3b  17529  yonedainv  17531  ismhm  17958  prdspjmhm  17993  isgrpinv  18156  pwsmulg  18272  isghm  18358  cayleylem2  18541  symgfix2  18544  gsmsymgrfix  18556  gsmsymgreq  18560  symgfixelq  18561  pmtr3ncomlem2  18602  pmtrdifel  18608  pmtrdifwrdel  18613  pmtrdifwrdel2  18614  psgnunilem2  18623  psgnunilem3  18624  efgsdm  18856  efgredlemd  18870  efgredlem  18873  efgred  18874  efgrelexlema  18875  efgrelexlemb  18876  prdsgsum  19101  isabv  19590  islmhm  19799  psrmulfval  20165  evlslem2  20292  evlslem3  20293  evlslem1  20295  mpfrcl  20298  selvval  20331  coe1fval  20373  coe1mul2lem2  20436  coe1tm  20441  frgpcyg  20720  psgndiflemB  20744  psgndiflemA  20745  dsmmelbas  20883  frlmipval  20923  frlmphl  20925  uvcf1  20936  islindf  20956  islindf4  20982  madetsumid  21070  mvmulval  21152  marepvval0  21175  mulmarep1gsum2  21183  mdetleib2  21197  m1detdiag  21206  mdetralt  21217  mdetunilem7  21227  mdetunilem9  21229  m2detleiblem3  21238  m2detleiblem4  21239  m2detleib  21240  symgmatr01lem  21262  gsummatr01lem1  21264  gsummatr01lem4  21267  gsummatr01  21268  smadiadetlem3  21277  pmatcoe1fsupp  21309  pmatcollpw3lem  21391  pmatcollpw3fi1lem2  21395  iscnp  21845  1stcfb  22053  ptpjpre1  22179  elpt  22180  elptr  22181  ptpjopn  22220  dfac14  22226  upxp  22231  pthaus  22246  ptrescn  22247  xkoptsub  22262  cnmptkp  22288  xkofvcn  22292  cnmptk1p  22293  cnmptk2  22294  ptunhmeo  22416  ptcmplem3  22662  ptcmplem4  22663  symgtgp  22714  prdstmdd  22732  isucn  22887  imasdsf1olem  22983  prdsxmslem2  23139  tngngp3  23265  nmoval  23324  elcncf  23497  ishtpy  23576  pcoval  23615  om1elbas  23636  elpi1i  23650  iscau  23879  rrxds  23996  rrxdsfival  24016  ehl1eudisval  24024  ehl2eudisval  24026  mbfi1fseqlem6  24321  mbfi1flimlem  24323  isibl  24366  deg1ldg  24686  deg1leb  24689  elply2  24786  elplyr  24791  ne0p  24797  coeeu  24815  coelem  24816  coeeq  24817  coeidlem  24827  elqaalem3  24910  qaa  24912  iaa  24914  aareccl  24915  aannenlem2  24918  aaliou2  24929  dchrptlem2  25841  dchrpt  25843  dchrsum2  25844  sumdchr2  25846  dchrvmaeq0  26080  rpvmasum2  26088  dchrisum0re  26089  ostth  26215  iscgrg  26298  isismt  26320  israg  26483  iseqlg  26653  brbtwn  26685  brbtwn2  26691  colinearalg  26696  axsegconlem1  26703  axsegcon  26713  ax5seglem5  26719  axpasch  26727  axlowdim  26747  axeuclidlem  26748  axcontlem1  26750  axcontlem2  26751  axcontlem5  26754  vtxdgfval  27249  1egrvtxdg1  27291  isewlk  27384  iswlk  27392  uspgr2wlkeq2  27428  iswlkon  27439  isclwlk  27554  iscrct  27571  iscycl  27572  iswwlks  27614  wwlknon  27635  wlkiswwlks2  27653  wwlksnredwwlkn0  27674  wlksnwwlknvbij  27687  wwlksnextproplem3  27690  wwlksnextprop  27691  umgr2wlk  27728  midwwlks2s3  27731  elwwlks2  27745  elwspths2spth  27746  rusgrnumwwlkslem  27748  rusgrnumwwlkb0  27750  rusgrnumwwlks  27753  isclwwlk  27762  clwlkclwwlklem1  27777  clwwlkn1loopb  27821  clwwlkel  27825  clwwlkf  27826  clwwlkf1  27828  isclwwlknon  27870  clwwlknon1  27876  s2elclwwlknon2  27883  clwwlkvbij  27892  uhgr3cyclex  27961  fusgreg2wsplem  28112  fusgr2wsp2nb  28113  fusgreghash2wsp  28117  2clwwlkel  28128  extwwlkfabel  28132  numclwwlk1lem2fv  28135  numclwwlk1lem2  28139  clwwlknonclwlknonf1o  28141  dlwwlknondlwlknonf1o  28144  numclwwlk2lem1  28155  numclwlk2lem2f  28156  numclwlk2lem2f1o  28158  ex-fv  28222  isnvlem  28387  islno  28530  nmooval  28540  nmblolbi  28577  isphg  28594  ajmoi  28635  ajval  28638  ubthlem3  28649  htthlem  28694  hcau  28961  hlimi  28965  hosmval  29512  hommval  29513  hodmval  29514  hfsmval  29515  hfmmval  29516  adjmo  29609  nmopval  29633  elcnop  29634  ellnop  29635  elunop  29649  elhmop  29650  nmfnval  29653  elcnfn  29659  ellnfn  29660  adjeu  29666  adjval  29667  eigvecval  29673  eigvalfval  29674  adj1  29710  adjeq  29712  hmopadj2  29718  lnopeq0i  29784  lnopeq  29786  elunop2  29790  lnophm  29796  hmopco  29800  nmbdoplb  29802  nmcoplb  29807  lnopcon  29812  lnfn0  29824  lnfnmul  29825  nmbdfnlb  29827  nmcfnlb  29831  lnfncon  29833  riesz4  29841  riesz1  29842  cnlnadjlem9  29852  cnlnadjeu  29855  cnlnssadj  29857  nmopcoi  29872  bra11  29885  cnvbraval  29887  pjss2coi  29941  pjssdif2i  29951  pjssdif1i  29952  pjclem4  29976  pj3si  29984  pj3cor1i  29986  isst  29990  ishst  29991  stri  30034  hstri  30042  aciunf1lem  30407  linds2eq  30941  lbsdiflsp0  31022  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  lmatval  31078  mdetpmtr1  31088  ismeas  31458  isrnmeas  31459  cntnevol  31487  carsgval  31561  sitgval  31590  eulerpartleme  31621  eulerpartlemd  31624  eulerpartlemr  31632  eulerpartlemgvv  31634  eulerpart  31640  cndprobval  31691  signstfvneq0  31842  reprsum  31884  reprsuc  31886  reprpmtf1o  31897  reprdifc  31898  breprexp  31904  vtsval  31908  hgt750lemb  31927  hgt750lema  31928  hgt750leme  31929  bnj66  32132  bnj106  32140  bnj125  32144  bnj154  32150  bnj155  32151  bnj526  32160  bnj540  32164  bnj609  32189  bnj611  32190  bnj893  32200  bnj1000  32213  bnj1014  32233  bnj1015  32234  bnj1234  32285  bnj1463  32327  loop1cycl  32384  derangenlem  32418  subfacp1lem3  32429  subfacp1lem5  32431  subfacp1lem6  32432  subfacp1  32433  sconnpht  32476  cnpconn  32477  txpconn  32479  ptpconn  32480  indispconn  32481  connpconn  32482  cvxpconn  32489  cvmliftmo  32531  cvmliftlem14  32544  cvmliftlem15  32545  cvmliftiota  32548  cvmlift2  32563  cvmliftphtlem  32564  cvmlift3lem2  32567  cvmlift3lem6  32571  cvmlift3lem7  32572  cvmlift3lem9  32574  cvmlift3  32575  satfv1lem  32609  satfv1  32610  sategoelfvb  32666  mrsubff1  32761  mrsub0  32763  mrsubccat  32765  mrsubcn  32766  elmsubrn  32775  msubrn  32776  msubco  32778  msubvrs  32807  mclsax  32816  shftvalg  32963  poseq  33095  soseq  33096  frrlem1  33123  frrlem13  33135  sltval  33154  nolesgn2o  33178  noresle  33200  noprefixmo  33202  nosupfv  33206  fwddifval  33623  fwddifnval  33624  bj-evalval  34369  unceq  34884  matunitlindflem2  34904  poimirlem17  34924  poimirlem20  34927  poimirlem22  34929  poimirlem23  34930  poimirlem27  34934  poimirlem28  34935  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  poimir  34940  broucube  34941  voliunnfl  34951  volsupnfl  34952  itg2addnclem  34958  itg2addnclem3  34960  itg2addnc  34961  ftc1anclem2  34983  ftc1anclem5  34986  eqfnun  35012  upixp  35019  fdc  35035  isismty  35094  rrnmval  35121  elghomlem2OLD  35179  isrngohom  35258  islfl  36211  isopos  36331  islaut  37234  ispautN  37250  isldil  37261  isltrn  37270  ltrnid  37286  ltrneq2  37299  isdilN  37305  istrnN  37308  trlval  37313  ltrneq3  37359  cdleme50ex  37710  cdleme  37711  cdlemg1a  37721  ltrniotaval  37732  ltrniotavalbN  37735  cdlemeiota  37736  cdlemg2jlemOLDN  37744  cdlemg2fvlem  37745  cdlemg2klem  37746  istendo  37911  tendoplcbv  37926  tendopl  37927  tendoicbv  37944  tendoi  37945  tendoid0  37976  tendo1ne0  37979  cdlemksv2  37998  cdlemkuv2  38018  cdlemk33N  38060  cdlemk34  38061  cdlemk36  38064  cdlemk19u  38121  cdlemk  38125  tendoex  38126  dvavsca  38168  dvhvscacbv  38249  dvhvscaval  38250  dicopelval  38328  dicelval1sta  38338  diclspsn  38345  dihmeetlem13N  38470  dih1dimatlem0  38479  dih1dimatlem  38480  dihpN  38487  islpolN  38634  hdmap1fval  38947  hdmapfval  38978  frlmsnic  39169  uvcn0  39171  ismrc  39318  mzpclval  39342  mzpsubst  39365  mzprename  39366  mzpcompact2lem  39368  eldioph  39375  eldioph2  39379  eldioph2b  39380  eldioph3  39383  rexrabdioph  39411  2rexfrabdioph  39413  3rexfrabdioph  39414  4rexfrabdioph  39415  6rexfrabdioph  39416  7rexfrabdioph  39417  eldioph4i  39429  rabren3dioph  39432  mzpcong  39589  jm2.27dlem1  39626  wepwsolem  39662  aomclem6  39679  aomclem8  39681  dfac11  39682  dgraalem  39765  dgraaub  39768  dgraa0p  39769  mpaaeu  39770  mpaalem  39772  aaitgo  39782  rngunsnply  39793  eliunov2  40044  rfovcnvfvd  40373  fsovfvd  40376  fsovcnvlem  40379  dssmapfv2d  40384  dssmapnvod  40386  clsk1independent  40416  ntrclskb  40439  ntrclsk13  40441  gneispace2  40502  dvconstbi  40686  addrval  40818  subrval  40819  mulvval  40820  fnchoice  41306  refsum2cnlem1  41314  choicefi  41483  axccdom  41507  fmulcl  41882  fmuldfeqlem1  41883  mccllem  41898  mccl  41899  climf  41923  climf2  41967  dvnprodlem1  42251  dvnprodlem3  42253  dvnprod  42254  stoweidlem2  42307  stoweidlem6  42311  stoweidlem8  42313  stoweidlem9  42314  stoweidlem15  42320  stoweidlem16  42321  stoweidlem17  42322  stoweidlem18  42323  stoweidlem21  42326  stoweidlem27  42332  stoweidlem31  42336  stoweidlem36  42341  stoweidlem37  42342  stoweidlem41  42346  stoweidlem43  42348  stoweidlem44  42349  stoweidlem45  42350  stoweidlem46  42351  stoweidlem48  42353  stoweidlem51  42356  stoweidlem55  42360  stoweidlem59  42364  stoweidlem60  42365  stoweidlem62  42367  fourierdlem2  42414  fourierdlem3  42415  elaa2lem  42538  etransclem11  42550  etransclem24  42563  etransclem26  42565  etransclem28  42567  etransclem35  42574  rrndistlt  42595  ioorrnopn  42610  subsaliuncllem  42660  sge0val  42668  ismea  42753  caragenval  42795  isome  42796  isomenndlem  42832  hoicvrrex  42858  ovnlecvr  42860  ovncvrrp  42866  ovn0lem  42867  ovnsubaddlem1  42872  ovnsubadd  42874  hsphoif  42878  hoidmvval  42879  hsphoival  42881  hoidmvlelem3  42899  hoidmvlelem5  42901  hoidmvle  42902  ovnhoilem1  42903  ovnhoi  42905  ovnlecvr2  42912  ovncvr2  42913  hoidifhspval2  42917  hoiqssbllem2  42925  hspmbllem2  42929  hspmbllem3  42930  hspmbl  42931  ovnovollem1  42958  smfmullem2  43087  smfmul  43090  smfpimcclem  43101  iccpart  43596  iccpartiun  43614  icceuelpart  43616  nnsum3primes4  43973  nnsum3primesgbe  43977  nnsum4primesodd  43981  nnsum4primesoddALTV  43982  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  bgoldbtbnd  43994  isomgreqve  44010  isomushgr  44011  isomuspgrlem2  44018  isomgrsym  44021  isomgrtr  44024  ushrisomgr  44026  isupwlk  44031  ismgmhm  44070  isrnghm  44183  lincval  44484  lincdifsn  44499  linindslinci  44523  lindslinindsimp1  44532  linds0  44540  el0ldep  44541  lindsrng01  44543  snlindsntorlem  44545  ldepspr  44548  islindeps2  44558  zlmodzxzldep  44579  bigoval  44629  elbigo  44631  prelrrx2b  44721  rrx2plord  44727  rrx2vlinest  44748  rrx2linesl  44750  elrrx2linest2  44752  line2ylem  44758  line2xlem  44760  itsclc0  44778  itsclc0b  44779  itscnhlinecirc02p  44792  setrecseq  44808  aacllem  44922