Theorem fveq1 6755

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5070  ℩cio 6374  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426

This theorem is referenced by:  fveq1i  6757  fveq1d  6758  iffv  6773  fvmptd3f  6872  fvmptdv2  6875  fsnex  7135  f1prex  7136  isoeq1  7168  oveq  7261  elovmpt3imp  7504  ofrfvalg  7519  offval  7520  offval3  7798  bropopvvv  7901  bropfvvvvlem  7902  frrlem1  8073  frrlem13  8085  wfrlem1OLD  8110  wfrlem3OLDa  8113  wfrlem15OLD  8125  smoeq  8152  tfrlem12  8191  tz7.44-2  8209  tz7.44-3  8210  rdgeq1  8213  fsetfocdm  8607  fsetprcnex  8608  mapsncnv  8639  elixp2  8647  resixpfo  8682  elixpsn  8683  mapsnend  8780  enfixsn  8821  mapxpen  8879  ac6sfi  8988  ordtypelem7  9213  wemaplem1  9235  ixpiunwdom  9279  oemapval  9371  cantnf  9381  wemapwe  9385  cnfcom3clem  9393  updjud  9623  infxpenc2lem2  9707  fseqenlem1  9711  dfac8clem  9719  ac5num  9723  acni  9732  acni2  9733  acnlem  9735  dfac4  9809  dfac5lem5  9814  dfac2a  9816  dfac9  9823  dfacacn  9828  dfac12lem1  9830  dfac12r  9833  cofsmo  9956  cfsmolem  9957  cfsmo  9958  cfcoflem  9959  coftr  9960  alephsing  9963  isfin3ds  10016  fin23lem17  10025  fin23lem32  10031  fin23lem39  10037  isf33lem  10053  isf34lem6  10067  axcc2lem  10123  axcc3  10125  axdc2lem  10135  axdc3lem2  10138  axdc3lem3  10139  axdc3  10141  axdc4lem  10142  axcclem  10144  ac6num  10166  axdclem2  10207  konigthlem  10255  inar1  10462  1fv  13304  axdc4uzlem  13631  seqeq3  13654  seqof  13708  ccatfval  14204  wrdl1s1  14247  ccat1st1st  14263  cshf1  14451  cshweqrep  14462  wrdlen2i  14583  wwlktovf  14599  wwlktovf1  14600  wwlktovfo  14601  wrd2f1tovbij  14603  rtrclreclem1  14696  dfrtrclrec2  14697  rtrclreclem2  14698  rtrclreclem4  14700  dfrtrcl2  14701  clim  15131  rlim  15132  ello1  15152  elo1  15163  summo  15357  fsum  15360  prodmo  15574  fprod  15579  bpolylem  15686  bpolyval  15687  vdwlem6  16615  vdwlem8  16617  ramcl  16658  strfvnd  16814  prdsplusgval  17101  prdsmulrval  17103  prdsleval  17105  prdsdsval  17106  prdsvscaval  17107  xpsff1o  17195  isacs2  17279  isnat  17579  yonedalem3b  17913  yonedainv  17915  ismhm  18347  prdspjmhm  18382  isgrpinv  18547  pwsmulg  18663  isghm  18749  cayleylem2  18936  symgfix2  18939  gsmsymgrfix  18951  gsmsymgreq  18955  symgfixelq  18956  pmtr3ncomlem2  18997  pmtrdifel  19003  pmtrdifwrdel  19008  pmtrdifwrdel2  19009  psgnunilem2  19018  psgnunilem3  19019  efgsdm  19251  efgredlemd  19265  efgredlem  19268  efgred  19269  efgrelexlema  19270  efgrelexlemb  19271  prdsgsum  19497  isabv  19994  islmhm  20204  frgpcyg  20693  psgndiflemB  20717  psgndiflemA  20718  dsmmelbas  20856  frlmipval  20896  frlmphl  20898  uvcf1  20909  islindf  20929  islindf4  20955  psrmulfval  21064  evlslem2  21199  evlslem3  21200  evlslem1  21202  mpfrcl  21205  selvval  21238  coe1fval  21286  coe1mul2lem2  21349  coe1tm  21354  madetsumid  21518  mvmulval  21600  marepvval0  21623  mulmarep1gsum2  21631  mdetleib2  21645  m1detdiag  21654  mdetralt  21665  mdetunilem7  21675  mdetunilem9  21677  m2detleiblem3  21686  m2detleiblem4  21687  m2detleib  21688  symgmatr01lem  21710  gsummatr01lem1  21712  gsummatr01lem4  21715  gsummatr01  21716  smadiadetlem3  21725  pmatcoe1fsupp  21758  pmatcollpw3lem  21840  pmatcollpw3fi1lem2  21844  iscnp  22296  1stcfb  22504  ptpjpre1  22630  elpt  22631  elptr  22632  ptpjopn  22671  dfac14  22677  upxp  22682  pthaus  22697  ptrescn  22698  xkoptsub  22713  cnmptkp  22739  xkofvcn  22743  cnmptk1p  22744  cnmptk2  22745  ptunhmeo  22867  ptcmplem3  23113  ptcmplem4  23114  symgtgp  23165  prdstmdd  23183  isucn  23338  imasdsf1olem  23434  prdsxmslem2  23591  tngngp3  23726  nmoval  23785  elcncf  23958  ishtpy  24041  pcoval  24080  om1elbas  24101  elpi1i  24115  iscau  24345  rrxds  24462  rrxdsfival  24482  ehl1eudisval  24490  ehl2eudisval  24492  mbfi1fseqlem6  24790  mbfi1flimlem  24792  isibl  24835  deg1ldg  25162  deg1leb  25165  elply2  25262  elplyr  25267  ne0p  25273  coeeu  25291  coelem  25292  coeeq  25293  coeidlem  25303  elqaalem3  25386  qaa  25388  iaa  25390  aareccl  25391  aannenlem2  25394  aaliou2  25405  dchrptlem2  26318  dchrpt  26320  dchrsum2  26321  sumdchr2  26323  dchrvmaeq0  26557  rpvmasum2  26565  dchrisum0re  26566  ostth  26692  iscgrg  26777  isismt  26799  israg  26962  iseqlg  27132  brbtwn  27170  brbtwn2  27176  colinearalg  27181  axsegconlem1  27188  axsegcon  27198  ax5seglem5  27204  axpasch  27212  axlowdim  27232  axeuclidlem  27233  axcontlem1  27235  axcontlem2  27236  axcontlem5  27239  vtxdgfval  27737  1egrvtxdg1  27779  isewlk  27872  iswlk  27880  uspgr2wlkeq2  27916  iswlkon  27927  isclwlk  28042  iscrct  28059  iscycl  28060  iswwlks  28102  wwlknon  28123  wlkiswwlks2  28141  wwlksnredwwlkn0  28162  wlksnwwlknvbij  28174  wwlksnextproplem3  28177  wwlksnextprop  28178  umgr2wlk  28215  midwwlks2s3  28218  elwwlks2  28232  elwspths2spth  28233  rusgrnumwwlkslem  28235  rusgrnumwwlkb0  28237  rusgrnumwwlks  28240  isclwwlk  28249  clwlkclwwlklem1  28264  clwwlkn1loopb  28308  clwwlkel  28311  clwwlkf  28312  clwwlkf1  28314  isclwwlknon  28356  clwwlknon1  28362  s2elclwwlknon2  28369  clwwlkvbij  28378  uhgr3cyclex  28447  fusgreg2wsplem  28598  fusgr2wsp2nb  28599  fusgreghash2wsp  28603  2clwwlkel  28614  extwwlkfabel  28618  numclwwlk1lem2fv  28621  numclwwlk1lem2  28625  clwwlknonclwlknonf1o  28627  dlwwlknondlwlknonf1o  28630  numclwwlk2lem1  28641  numclwlk2lem2f  28642  numclwlk2lem2f1o  28644  ex-fv  28708  isnvlem  28873  islno  29016  nmooval  29026  nmblolbi  29063  isphg  29080  ajmoi  29121  ajval  29124  ubthlem3  29135  htthlem  29180  hcau  29447  hlimi  29451  hosmval  29998  hommval  29999  hodmval  30000  hfsmval  30001  hfmmval  30002  adjmo  30095  nmopval  30119  elcnop  30120  ellnop  30121  elunop  30135  elhmop  30136  nmfnval  30139  elcnfn  30145  ellnfn  30146  adjeu  30152  adjval  30153  eigvecval  30159  eigvalfval  30160  adj1  30196  adjeq  30198  hmopadj2  30204  lnopeq0i  30270  lnopeq  30272  elunop2  30276  lnophm  30282  hmopco  30286  nmbdoplb  30288  nmcoplb  30293  lnopcon  30298  lnfn0  30310  lnfnmul  30311  nmbdfnlb  30313  nmcfnlb  30317  lnfncon  30319  riesz4  30327  riesz1  30328  cnlnadjlem9  30338  cnlnadjeu  30341  cnlnssadj  30343  nmopcoi  30358  bra11  30371  cnvbraval  30373  pjss2coi  30427  pjssdif2i  30437  pjssdif1i  30438  pjclem4  30462  pj3si  30470  pj3cor1i  30472  isst  30476  ishst  30477  stri  30520  hstri  30528  aciunf1lem  30901  ismnt  31163  mgcval  31167  linds2eq  31477  elrspunidl  31508  lbsdiflsp0  31609  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  lmatval  31665  mdetpmtr1  31675  zarcmplem  31733  ismeas  32067  isrnmeas  32068  cntnevol  32096  carsgval  32170  sitgval  32199  eulerpartleme  32230  eulerpartlemd  32233  eulerpartlemr  32241  eulerpartlemgvv  32243  eulerpart  32249  cndprobval  32300  signstfvneq0  32451  reprsum  32493  reprsuc  32495  reprpmtf1o  32506  reprdifc  32507  breprexp  32513  vtsval  32517  hgt750lemb  32536  hgt750lema  32537  hgt750leme  32538  bnj66  32740  bnj106  32748  bnj125  32752  bnj154  32758  bnj155  32759  bnj526  32768  bnj540  32772  bnj609  32797  bnj611  32798  bnj893  32808  bnj1000  32821  bnj1014  32841  bnj1015  32842  bnj1234  32893  bnj1463  32935  loop1cycl  32999  derangenlem  33033  subfacp1lem3  33044  subfacp1lem5  33046  subfacp1lem6  33047  subfacp1  33048  sconnpht  33091  cnpconn  33092  txpconn  33094  ptpconn  33095  indispconn  33096  connpconn  33097  cvxpconn  33104  cvmliftmo  33146  cvmliftlem14  33159  cvmliftlem15  33160  cvmliftiota  33163  cvmlift2  33178  cvmliftphtlem  33179  cvmlift3lem2  33182  cvmlift3lem6  33186  cvmlift3lem7  33187  cvmlift3lem9  33189  cvmlift3  33190  satfv1lem  33224  satfv1  33225  sategoelfvb  33281  mrsubff1  33376  mrsub0  33378  mrsubccat  33380  mrsubcn  33381  elmsubrn  33390  msubrn  33391  msubco  33393  msubvrs  33422  mclsax  33431  shftvalg  33603  ssttrcl  33701  ttrcltr  33702  ttrclss  33706  ttrclselem2  33712  poseq  33729  soseq  33730  sltval  33777  nolesgn2o  33801  nogesgn1o  33803  noresle  33827  nosupprefixmo  33830  noinfprefixmo  33831  nosupcbv  33832  nosupfv  33836  noinfcbv  33847  noinffv  33851  fwddifval  34391  fwddifnval  34392  bj-evalval  35173  unceq  35681  matunitlindflem2  35701  poimirlem17  35721  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem27  35731  poimirlem28  35732  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  poimir  35737  broucube  35738  voliunnfl  35748  volsupnfl  35749  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  ftc1anclem2  35778  ftc1anclem5  35781  eqfnun  35807  upixp  35814  fdc  35830  isismty  35886  rrnmval  35913  elghomlem2OLD  35971  isrngohom  36050  islfl  37001  isopos  37121  islaut  38024  ispautN  38040  isldil  38051  isltrn  38060  ltrnid  38076  ltrneq2  38089  isdilN  38095  istrnN  38098  trlval  38103  ltrneq3  38149  cdleme50ex  38500  cdleme  38501  cdlemg1a  38511  ltrniotaval  38522  ltrniotavalbN  38525  cdlemeiota  38526  cdlemg2jlemOLDN  38534  cdlemg2fvlem  38535  cdlemg2klem  38536  istendo  38701  tendoplcbv  38716  tendopl  38717  tendoicbv  38734  tendoi  38735  tendoid0  38766  tendo1ne0  38769  cdlemksv2  38788  cdlemkuv2  38808  cdlemk33N  38850  cdlemk34  38851  cdlemk36  38854  cdlemk19u  38911  cdlemk  38915  tendoex  38916  dvavsca  38958  dvhvscacbv  39039  dvhvscaval  39040  dicopelval  39118  dicelval1sta  39128  diclspsn  39135  dihmeetlem13N  39260  dih1dimatlem0  39269  dih1dimatlem  39270  dihpN  39277  islpolN  39424  hdmap1fval  39737  hdmapfval  39768  sticksstones1  40030  sticksstones2  40031  sticksstones3  40032  sticksstones8  40037  sticksstones10  40039  sticksstones11  40040  sticksstones12a  40041  sticksstones12  40042  sticksstones15  40045  frlmsnic  40188  uvcn0  40190  pwspjmhmmgpd  40192  pwsexpg  40193  pwsgprod  40194  evlsvarval  40197  evlsbagval  40198  fsuppssindlem2  40204  fsuppssind  40205  prjspnfv01  40382  prjspner01  40383  prjspner1  40384  ismrc  40439  mzpclval  40463  mzpsubst  40486  mzprename  40487  mzpcompact2lem  40489  eldioph  40496  eldioph2  40500  eldioph2b  40501  eldioph3  40504  rexrabdioph  40532  2rexfrabdioph  40534  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  eldioph4i  40550  rabren3dioph  40553  mzpcong  40710  jm2.27dlem1  40747  wepwsolem  40783  aomclem6  40800  aomclem8  40802  dfac11  40803  dgraalem  40886  dgraaub  40889  dgraa0p  40890  mpaaeu  40891  mpaalem  40893  aaitgo  40903  rngunsnply  40914  eliunov2  41176  rfovcnvfvd  41504  fsovfvd  41507  fsovcnvlem  41510  dssmapfv2d  41515  dssmapnvod  41517  clsk1independent  41545  ntrclskb  41568  ntrclsk13  41570  gneispace2  41631  mnringmulrvald  41734  dvconstbi  41841  addrval  41973  subrval  41974  mulvval  41975  fnchoice  42461  refsum2cnlem1  42469  choicefi  42629  axccdom  42651  fmulcl  43012  fmuldfeqlem1  43013  mccllem  43028  mccl  43029  climf  43053  climf2  43097  dvnprodlem1  43377  dvnprodlem3  43379  dvnprod  43380  stoweidlem2  43433  stoweidlem6  43437  stoweidlem8  43439  stoweidlem9  43440  stoweidlem15  43446  stoweidlem16  43447  stoweidlem17  43448  stoweidlem18  43449  stoweidlem21  43452  stoweidlem27  43458  stoweidlem31  43462  stoweidlem36  43467  stoweidlem37  43468  stoweidlem41  43472  stoweidlem43  43474  stoweidlem44  43475  stoweidlem45  43476  stoweidlem46  43477  stoweidlem48  43479  stoweidlem51  43482  stoweidlem55  43486  stoweidlem59  43490  stoweidlem60  43491  stoweidlem62  43493  fourierdlem2  43540  fourierdlem3  43541  elaa2lem  43664  etransclem11  43676  etransclem24  43689  etransclem26  43691  etransclem28  43693  etransclem35  43700  rrndistlt  43721  ioorrnopn  43736  subsaliuncllem  43786  sge0val  43794  ismea  43879  caragenval  43921  isome  43922  isomenndlem  43958  hoicvrrex  43984  ovnlecvr  43986  ovncvrrp  43992  ovn0lem  43993  ovnsubaddlem1  43998  ovnsubadd  44000  hsphoif  44004  hoidmvval  44005  hsphoival  44007  hoidmvlelem3  44025  hoidmvlelem5  44027  hoidmvle  44028  ovnhoilem1  44029  ovnhoi  44031  ovnlecvr2  44038  ovncvr2  44039  hoidifhspval2  44043  hoiqssbllem2  44051  hspmbllem2  44055  hspmbllem3  44056  hspmbl  44057  ovnovollem1  44084  smfmullem2  44213  smfmul  44216  smfpimcclem  44227  cfsetsnfsetfv  44438  cfsetsnfsetfo  44441  iccpart  44756  iccpartiun  44774  icceuelpart  44776  nnsum3primes4  45128  nnsum3primesgbe  45132  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  bgoldbtbnd  45149  isomgreqve  45165  isomushgr  45166  isomuspgrlem2  45173  isomgrsym  45176  isomgrtr  45179  ushrisomgr  45181  isupwlk  45186  ismgmhm  45225  isrnghm  45338  lincval  45638  lincdifsn  45653  linindslinci  45677  lindslinindsimp1  45686  linds0  45694  el0ldep  45695  lindsrng01  45697  snlindsntorlem  45699  ldepspr  45702  islindeps2  45712  zlmodzxzldep  45733  bigoval  45783  elbigo  45785  0aryfvalelfv  45869  1arympt1fv  45873  1arymaptfv  45874  1arymaptfo  45877  2arymptfv  45884  2arymaptfv  45885  2arymaptfo  45888  prelrrx2b  45948  rrx2plord  45954  rrx2vlinest  45975  rrx2linesl  45977  elrrx2linest2  45979  line2ylem  45985  line2xlem  45987  itsclc0  46005  itsclc0b  46006  itscnhlinecirc02p  46019  elfvne0  46064  thincciso  46218  setrecseq  46277  aacllem  46391