Theorem fveq1 6821

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5092  ℩cio 6436  ‘cfv 6482

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 3438  df-ss 3920  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490

This theorem is referenced by:  fveq1i  6823  fveq1d  6824  iffv  6839  fvmptd3f  6945  fvmptdv2  6948  eqfnun  6971  fsnex  7220  f1prex  7221  isoeq1  7254  oveq  7355  elovmpt3imp  7606  ofrfvalg  7621  offval  7622  offval3  7917  bropopvvv  8023  bropfvvvvlem  8024  poseq  8091  soseq  8092  frrlem1  8219  frrlem13  8231  smoeq  8273  tfrlem12  8311  tz7.44-2  8329  tz7.44-3  8330  rdgeq1  8333  fsetfocdm  8788  fsetprcnex  8789  mapsncnv  8820  elixp2  8828  resixpfo  8863  elixpsn  8864  mapsnend  8961  enfixsn  9003  mapxpen  9060  ac6sfi  9173  ordtypelem7  9416  wemaplem1  9438  ixpiunwdom  9482  oemapval  9579  cantnf  9589  wemapwe  9593  cnfcom3clem  9601  ssttrcl  9611  ttrcltr  9612  ttrclss  9616  ttrclselem2  9622  updjud  9830  infxpenc2lem2  9914  fseqenlem1  9918  dfac8clem  9926  ac5num  9930  acni  9939  acni2  9940  acnlem  9942  dfac4  10016  dfac5lem5  10021  dfac2a  10024  dfac9  10031  dfacacn  10036  dfac12lem1  10038  dfac12r  10041  cofsmo  10163  cfsmolem  10164  cfsmo  10165  cfcoflem  10166  coftr  10167  alephsing  10170  isfin3ds  10223  fin23lem17  10232  fin23lem32  10238  fin23lem39  10244  isf33lem  10260  isf34lem6  10274  axcc2lem  10330  axcc3  10332  axdc2lem  10342  axdc3lem2  10345  axdc3lem3  10346  axdc3  10348  axdc4lem  10349  axcclem  10351  ac6num  10373  axdclem2  10414  konigthlem  10462  inar1  10669  1fv  13550  axdc4uzlem  13890  seqeq3  13913  seqof  13966  ccatfval  14480  wrdl1s1  14521  ccat1st1st  14535  cshf1  14716  cshweqrep  14727  wrdlen2i  14849  wwlktovf  14863  wwlktovf1  14864  wwlktovfo  14865  wrd2f1tovbij  14867  rtrclreclem1  14964  dfrtrclrec2  14965  rtrclreclem2  14966  rtrclreclem4  14968  dfrtrcl2  14969  clim  15401  rlim  15402  ello1  15422  elo1  15433  summo  15624  fsum  15627  prodmo  15843  fprod  15848  bpolylem  15955  bpolyval  15956  vdwlem6  16898  vdwlem8  16900  ramcl  16941  strfvnd  17096  prdsplusgval  17377  prdsmulrval  17379  prdsleval  17381  prdsdsval  17382  prdsvscaval  17383  xpsff1o  17471  isacs2  17559  isnat  17857  yonedalem3b  18185  yonedainv  18187  ismgmhm  18570  ismhm  18659  prdspjmhm  18703  isgrpinv  18872  pwsmulg  18998  isghm  19094  isghmOLD  19095  cayleylem2  19292  symgfix2  19295  gsmsymgrfix  19307  gsmsymgreq  19311  symgfixelq  19312  pmtr3ncomlem2  19353  pmtrdifel  19359  pmtrdifwrdel  19364  pmtrdifwrdel2  19365  psgnunilem2  19374  psgnunilem3  19375  efgsdm  19609  efgredlemd  19623  efgredlem  19626  efgred  19627  efgrelexlema  19628  efgrelexlemb  19629  prdsgsum  19860  pwspjmhmmgpd  20213  pwsexpg  20214  isrnghm  20326  isabv  20696  islmhm  20931  frgpcyg  21480  psgndiflemB  21507  psgndiflemA  21508  dsmmelbas  21646  frlmipval  21686  frlmphl  21688  uvcf1  21699  islindf  21719  islindf4  21745  psrmulfval  21850  evlslem2  21984  evlslem3  21985  evlslem1  21987  mpfrcl  21990  selvval  22020  psdval  22044  psdcoef  22045  psdadd  22048  psdmul  22051  psdmvr  22054  coe1fval  22088  coe1mul2lem2  22152  coe1tm  22157  madetsumid  22346  mvmulval  22428  marepvval0  22451  mulmarep1gsum2  22459  mdetleib2  22473  m1detdiag  22482  mdetralt  22493  mdetunilem7  22503  mdetunilem9  22505  m2detleiblem3  22514  m2detleiblem4  22515  m2detleib  22516  symgmatr01lem  22538  gsummatr01lem1  22540  gsummatr01lem4  22543  gsummatr01  22544  smadiadetlem3  22553  pmatcoe1fsupp  22586  pmatcollpw3lem  22668  pmatcollpw3fi1lem2  22672  iscnp  23122  1stcfb  23330  ptpjpre1  23456  elpt  23457  elptr  23458  ptpjopn  23497  dfac14  23503  upxp  23508  pthaus  23523  ptrescn  23524  xkoptsub  23539  cnmptkp  23565  xkofvcn  23569  cnmptk1p  23570  cnmptk2  23571  ptunhmeo  23693  ptcmplem3  23939  ptcmplem4  23940  symgtgp  23991  prdstmdd  24009  isucn  24163  imasdsf1olem  24259  prdsxmslem2  24415  tngngp3  24542  nmoval  24601  elcncf  24780  ishtpy  24869  pcoval  24909  om1elbas  24930  elpi1i  24944  iscau  25174  rrxds  25291  rrxdsfival  25311  ehl1eudisval  25319  ehl2eudisval  25321  mbfi1fseqlem6  25619  mbfi1flimlem  25621  isibl  25664  deg1ldg  25995  deg1leb  25998  elply2  26099  elplyr  26104  ne0p  26110  coeeu  26128  coelem  26129  coeeq  26130  coeidlem  26140  elqaalem3  26227  qaa  26229  iaa  26231  aareccl  26232  aannenlem2  26235  aaliou2  26246  dchrptlem2  27174  dchrpt  27176  dchrsum2  27177  sumdchr2  27179  dchrvmaeq0  27413  rpvmasum2  27421  dchrisum0re  27422  ostth  27548  sltval  27557  nolesgn2o  27581  nogesgn1o  27583  noresle  27607  nosupprefixmo  27610  noinfprefixmo  27611  nosupcbv  27612  nosupfv  27616  noinfcbv  27627  noinffv  27631  iscgrg  28457  isismt  28479  israg  28642  iseqlg  28812  brbtwn  28844  brbtwn2  28850  colinearalg  28855  axsegconlem1  28862  axsegcon  28872  ax5seglem5  28878  axpasch  28886  axlowdim  28906  axeuclidlem  28907  axcontlem1  28909  axcontlem2  28910  axcontlem5  28913  vtxdgfval  29413  1egrvtxdg1  29455  isewlk  29548  iswlk  29556  uspgr2wlkeq2  29592  iswlkon  29601  isclwlk  29718  iscrct  29735  iscycl  29736  iswwlks  29781  wwlknon  29802  wlkiswwlks2  29820  wwlksnredwwlkn0  29841  wlksnwwlknvbij  29853  wwlksnextproplem3  29856  wwlksnextprop  29857  umgr2wlk  29894  midwwlks2s3  29897  elwwlks2  29911  elwspths2spth  29912  rusgrnumwwlkslem  29914  rusgrnumwwlkb0  29916  rusgrnumwwlks  29919  isclwwlk  29928  clwlkclwwlklem1  29943  clwwlkn1loopb  29987  clwwlkel  29990  clwwlkf  29991  clwwlkf1  29993  isclwwlknon  30035  clwwlknon1  30041  s2elclwwlknon2  30048  clwwlkvbij  30057  uhgr3cyclex  30126  fusgreg2wsplem  30277  fusgr2wsp2nb  30278  fusgreghash2wsp  30282  2clwwlkel  30293  extwwlkfabel  30297  numclwwlk1lem2fv  30300  numclwwlk1lem2  30304  clwwlknonclwlknonf1o  30306  dlwwlknondlwlknonf1o  30309  numclwwlk2lem1  30320  numclwlk2lem2f  30321  numclwlk2lem2f1o  30323  ex-fv  30387  isnvlem  30554  islno  30697  nmooval  30707  nmblolbi  30744  isphg  30761  ajmoi  30802  ajval  30805  ubthlem3  30816  htthlem  30861  hcau  31128  hlimi  31132  hosmval  31679  hommval  31680  hodmval  31681  hfsmval  31682  hfmmval  31683  adjmo  31776  nmopval  31800  elcnop  31801  ellnop  31802  elunop  31816  elhmop  31817  nmfnval  31820  elcnfn  31826  ellnfn  31827  adjeu  31833  adjval  31834  eigvecval  31840  eigvalfval  31841  adj1  31877  adjeq  31879  hmopadj2  31885  lnopeq0i  31951  lnopeq  31953  elunop2  31957  lnophm  31963  hmopco  31967  nmbdoplb  31969  nmcoplb  31974  lnopcon  31979  lnfn0  31991  lnfnmul  31992  nmbdfnlb  31994  nmcfnlb  31998  lnfncon  32000  riesz4  32008  riesz1  32009  cnlnadjlem9  32019  cnlnadjeu  32022  cnlnssadj  32024  nmopcoi  32039  bra11  32052  cnvbraval  32054  pjss2coi  32108  pjssdif2i  32118  pjssdif1i  32119  pjclem4  32143  pj3si  32151  pj3cor1i  32153  isst  32157  ishst  32158  stri  32201  hstri  32209  aciunf1lem  32605  ismnt  32925  mgcval  32929  ischn  32948  chnind  32953  chnub  32954  fzo0pmtrlast  33034  elrgspnlem1  33182  elrgspnlem2  33183  elrgspnlem3  33184  elrgspnlem4  33185  elrgspn  33186  elrgspnsubrunlem1  33187  linds2eq  33318  elrspunidl  33365  elrspunsn  33366  dfufd2lem  33486  mplvrpmga  33546  lbsdiflsp0  33593  fedgmullem1  33596  fedgmullem2  33597  fedgmul  33598  fldextrspunlsplem  33640  fldextrspunlsp  33641  fldext2chn  33695  constrextdg2lem  33715  constrextdg2  33716  lmatval  33780  mdetpmtr1  33790  zarcmplem  33848  ismeas  34166  isrnmeas  34167  cntnevol  34195  carsgval  34271  sitgval  34300  eulerpartleme  34331  eulerpartlemd  34334  eulerpartlemr  34342  eulerpartlemgvv  34344  eulerpart  34350  cndprobval  34401  signstfvneq0  34540  reprsum  34581  reprsuc  34583  reprpmtf1o  34594  reprdifc  34595  breprexp  34601  vtsval  34605  hgt750lemb  34624  hgt750lema  34625  hgt750leme  34626  bnj66  34827  bnj106  34835  bnj125  34839  bnj154  34845  bnj155  34846  bnj526  34855  bnj540  34859  bnj609  34884  bnj611  34885  bnj893  34895  bnj1000  34908  bnj1014  34928  bnj1015  34929  bnj1234  34980  bnj1463  35022  gblacfnacd  35075  loop1cycl  35110  derangenlem  35144  subfacp1lem3  35155  subfacp1lem5  35157  subfacp1lem6  35158  subfacp1  35159  sconnpht  35202  cnpconn  35203  txpconn  35205  ptpconn  35206  indispconn  35207  connpconn  35208  cvxpconn  35215  cvmliftmo  35257  cvmliftlem14  35270  cvmliftlem15  35271  cvmliftiota  35274  cvmlift2  35289  cvmliftphtlem  35290  cvmlift3lem2  35293  cvmlift3lem6  35297  cvmlift3lem7  35298  cvmlift3lem9  35300  cvmlift3  35301  satfv1lem  35335  satfv1  35336  sategoelfvb  35392  mrsubff1  35487  mrsub0  35489  mrsubccat  35491  mrsubcn  35492  elmsubrn  35501  msubrn  35502  msubco  35504  msubvrs  35533  mclsax  35542  shftvalg  35705  fwddifval  36136  fwddifnval  36137  bj-evalval  37049  unceq  37577  matunitlindflem2  37597  poimirlem17  37617  poimirlem20  37620  poimirlem22  37622  poimirlem23  37623  poimirlem27  37627  poimirlem28  37628  poimirlem30  37630  poimirlem31  37631  poimirlem32  37632  poimir  37633  broucube  37634  voliunnfl  37644  volsupnfl  37645  itg2addnclem  37651  itg2addnclem3  37653  itg2addnc  37654  ftc1anclem2  37674  ftc1anclem5  37677  upixp  37709  fdc  37725  isismty  37781  rrnmval  37808  elghomlem2OLD  37866  isrngohom  37945  islfl  39039  isopos  39159  islaut  40062  ispautN  40078  isldil  40089  isltrn  40098  ltrnid  40114  ltrneq2  40127  isdilN  40133  istrnN  40136  trlval  40141  ltrneq3  40187  cdleme50ex  40538  cdleme  40539  cdlemg1a  40549  ltrniotaval  40560  ltrniotavalbN  40563  cdlemeiota  40564  cdlemg2jlemOLDN  40572  cdlemg2fvlem  40573  cdlemg2klem  40574  istendo  40739  tendoplcbv  40754  tendopl  40755  tendoicbv  40772  tendoi  40773  tendoid0  40804  tendo1ne0  40807  cdlemksv2  40826  cdlemkuv2  40846  cdlemk33N  40888  cdlemk34  40889  cdlemk36  40892  cdlemk19u  40949  cdlemk  40953  tendoex  40954  dvavsca  40996  dvhvscacbv  41077  dvhvscaval  41078  dicopelval  41156  dicelval1sta  41166  diclspsn  41173  dihmeetlem13N  41298  dih1dimatlem0  41307  dih1dimatlem  41308  dihpN  41315  islpolN  41462  hdmap1fval  41775  hdmapfval  41806  sticksstones1  42119  sticksstones2  42120  sticksstones3  42121  sticksstones8  42126  sticksstones10  42128  sticksstones11  42129  sticksstones12a  42130  sticksstones12  42131  sticksstones15  42134  frlmsnic  42513  uvcn0  42515  pwsgprod  42517  mplmapghm  42529  evlsvval  42533  evlsvvval  42536  evlsvarval  42538  evlsbagval  42539  selvvvval  42558  evlselv  42560  fsuppssindlem2  42565  fsuppssind  42566  prjspnfv01  42597  prjspner01  42598  prjspner1  42599  sn-isghm  42646  ismrc  42674  mzpclval  42698  mzpsubst  42721  mzprename  42722  mzpcompact2lem  42724  eldioph  42731  eldioph2  42735  eldioph2b  42736  eldioph3  42739  rexrabdioph  42767  2rexfrabdioph  42769  3rexfrabdioph  42770  4rexfrabdioph  42771  6rexfrabdioph  42772  7rexfrabdioph  42773  eldioph4i  42785  rabren3dioph  42788  mzpcong  42945  jm2.27dlem1  42982  wepwsolem  43015  aomclem6  43032  aomclem8  43034  dfac11  43035  dgraalem  43118  dgraaub  43121  dgraa0p  43122  mpaaeu  43123  mpaalem  43125  aaitgo  43135  rngunsnply  43142  cantnfresb  43297  tfsconcatun  43310  nvocnvb  43395  eliunov2  43652  rfovcnvfvd  43980  fsovfvd  43983  fsovcnvlem  43986  dssmapfv2d  43991  dssmapnvod  43993  clsk1independent  44019  ntrclskb  44042  ntrclsk13  44044  gneispace2  44105  mnringmulrvald  44200  dvconstbi  44307  addrval  44439  subrval  44440  mulvval  44441  relpeq1  44918  fnchoice  45007  refsum2cnlem1  45015  choicefi  45178  axccdom  45200  fmulcl  45562  fmuldfeqlem1  45563  mccllem  45578  mccl  45579  climf  45603  climf2  45647  dvnprodlem1  45927  dvnprodlem3  45929  dvnprod  45930  stoweidlem2  45983  stoweidlem6  45987  stoweidlem8  45989  stoweidlem9  45990  stoweidlem15  45996  stoweidlem16  45997  stoweidlem17  45998  stoweidlem18  45999  stoweidlem21  46002  stoweidlem27  46008  stoweidlem31  46012  stoweidlem36  46017  stoweidlem37  46018  stoweidlem41  46022  stoweidlem43  46024  stoweidlem44  46025  stoweidlem45  46026  stoweidlem46  46027  stoweidlem48  46029  stoweidlem51  46032  stoweidlem55  46036  stoweidlem59  46040  stoweidlem60  46041  stoweidlem62  46043  fourierdlem2  46090  fourierdlem3  46091  elaa2lem  46214  etransclem11  46226  etransclem24  46239  etransclem26  46241  etransclem28  46243  etransclem35  46250  rrndistlt  46271  ioorrnopn  46286  subsaliuncllem  46338  sge0val  46347  ismea  46432  caragenval  46474  isome  46475  isomenndlem  46511  hoicvrrex  46537  ovnlecvr  46539  ovncvrrp  46545  ovn0lem  46546  ovnsubaddlem1  46551  ovnsubadd  46553  hsphoif  46557  hoidmvval  46558  hsphoival  46560  hoidmvlelem3  46578  hoidmvlelem5  46580  hoidmvle  46581  ovnhoilem1  46582  ovnhoi  46584  ovnlecvr2  46591  ovncvr2  46592  hoidifhspval2  46596  hoiqssbllem2  46604  hspmbllem2  46608  hspmbllem3  46609  hspmbl  46610  ovnovollem1  46637  smfmullem2  46773  smfmul  46776  smfpimcclem  46788  tworepnotupword  46867  sinnpoly  46875  cfsetsnfsetfv  47041  cfsetsnfsetfo  47044  iccpart  47400  iccpartiun  47418  icceuelpart  47420  nnsum3primes4  47772  nnsum3primesgbe  47776  nnsum4primesodd  47780  nnsum4primesoddALTV  47781  nnsum4primeseven  47784  nnsum4primesevenALTV  47785  bgoldbtbnd  47793  isisubgr  47846  isgrim  47866  grimidvtxedg  47869  grimcnv  47872  grimco  47873  isuspgrim0  47878  gricushgr  47901  ushggricedg  47911  uhgrimisgrgric  47915  isgrtri  47927  isubgr3stgrlem3  47952  isubgr3stgr  47959  isgrlim  47966  uspgrlim  47976  grlicref  47996  grlicsym  47997  grlictr  47999  grlimedgnedg  48115  isupwlk  48120  lincval  48394  lincdifsn  48409  linindslinci  48433  lindslinindsimp1  48442  linds0  48450  el0ldep  48451  lindsrng01  48453  snlindsntorlem  48455  ldepspr  48458  islindeps2  48468  zlmodzxzldep  48489  bigoval  48534  elbigo  48536  0aryfvalelfv  48620  1arympt1fv  48624  1arymaptfv  48625  1arymaptfo  48628  2arymptfv  48635  2arymaptfv  48636  2arymaptfo  48639  prelrrx2b  48699  rrx2plord  48705  rrx2vlinest  48726  rrx2linesl  48728  elrrx2linest2  48730  line2ylem  48736  line2xlem  48738  itsclc0  48756  itsclc0b  48757  itscnhlinecirc02p  48770  elfvne0  48833  iinfprg  49044  thincciso  49438  thinccisod  49439  setrecseq  49670  aacllem  49786