Theorem fveq1 6919

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 5168	. . 3 ⊢ (𝐹 = 𝐺 → (𝐴𝐹𝑥 ↔ 𝐴𝐺𝑥))
2	1	iotabidv 6557	. 2 ⊢ (𝐹 = 𝐺 → (℩𝑥𝐴𝐹𝑥) = (℩𝑥𝐴𝐺𝑥))
3		df-fv 6581	. 2 ⊢ (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)
4		df-fv 6581	. 2 ⊢ (𝐺‘𝐴) = (℩𝑥𝐴𝐺𝑥)
5	2, 3, 4	3eqtr4g 2805	1 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5166  ℩cio 6523  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581

This theorem is referenced by:  fveq1i  6921  fveq1d  6922  iffv  6937  fvmptd3f  7044  fvmptdv2  7047  eqfnun  7070  fsnex  7319  f1prex  7320  isoeq1  7353  oveq  7454  elovmpt3imp  7707  ofrfvalg  7722  offval  7723  offval3  8023  bropopvvv  8131  bropfvvvvlem  8132  poseq  8199  soseq  8200  frrlem1  8327  frrlem13  8339  wfrlem1OLD  8364  wfrlem3OLDa  8367  wfrlem15OLD  8379  smoeq  8406  tfrlem12  8445  tz7.44-2  8463  tz7.44-3  8464  rdgeq1  8467  fsetfocdm  8919  fsetprcnex  8920  mapsncnv  8951  elixp2  8959  resixpfo  8994  elixpsn  8995  mapsnend  9101  enfixsn  9147  mapxpen  9209  ac6sfi  9348  ordtypelem7  9593  wemaplem1  9615  ixpiunwdom  9659  oemapval  9752  cantnf  9762  wemapwe  9766  cnfcom3clem  9774  ssttrcl  9784  ttrcltr  9785  ttrclss  9789  ttrclselem2  9795  updjud  10003  infxpenc2lem2  10089  fseqenlem1  10093  dfac8clem  10101  ac5num  10105  acni  10114  acni2  10115  acnlem  10117  dfac4  10191  dfac5lem5  10196  dfac2a  10199  dfac9  10206  dfacacn  10211  dfac12lem1  10213  dfac12r  10216  cofsmo  10338  cfsmolem  10339  cfsmo  10340  cfcoflem  10341  coftr  10342  alephsing  10345  isfin3ds  10398  fin23lem17  10407  fin23lem32  10413  fin23lem39  10419  isf33lem  10435  isf34lem6  10449  axcc2lem  10505  axcc3  10507  axdc2lem  10517  axdc3lem2  10520  axdc3lem3  10521  axdc3  10523  axdc4lem  10524  axcclem  10526  ac6num  10548  axdclem2  10589  konigthlem  10637  inar1  10844  1fv  13704  axdc4uzlem  14034  seqeq3  14057  seqof  14110  ccatfval  14621  wrdl1s1  14662  ccat1st1st  14676  cshf1  14858  cshweqrep  14869  wrdlen2i  14991  wwlktovf  15005  wwlktovf1  15006  wwlktovfo  15007  wrd2f1tovbij  15009  rtrclreclem1  15106  dfrtrclrec2  15107  rtrclreclem2  15108  rtrclreclem4  15110  dfrtrcl2  15111  clim  15540  rlim  15541  ello1  15561  elo1  15572  summo  15765  fsum  15768  prodmo  15984  fprod  15989  bpolylem  16096  bpolyval  16097  vdwlem6  17033  vdwlem8  17035  ramcl  17076  strfvnd  17232  prdsplusgval  17533  prdsmulrval  17535  prdsleval  17537  prdsdsval  17538  prdsvscaval  17539  xpsff1o  17627  isacs2  17711  isnat  18015  yonedalem3b  18349  yonedainv  18351  ismgmhm  18734  ismhm  18820  prdspjmhm  18864  isgrpinv  19033  pwsmulg  19159  isghm  19255  isghmOLD  19256  cayleylem2  19455  symgfix2  19458  gsmsymgrfix  19470  gsmsymgreq  19474  symgfixelq  19475  pmtr3ncomlem2  19516  pmtrdifel  19522  pmtrdifwrdel  19527  pmtrdifwrdel2  19528  psgnunilem2  19537  psgnunilem3  19538  efgsdm  19772  efgredlemd  19786  efgredlem  19789  efgred  19790  efgrelexlema  19791  efgrelexlemb  19792  prdsgsum  20023  pwspjmhmmgpd  20351  pwsexpg  20352  isrnghm  20467  isabv  20834  islmhm  21049  frgpcyg  21615  psgndiflemB  21641  psgndiflemA  21642  dsmmelbas  21782  frlmipval  21822  frlmphl  21824  uvcf1  21835  islindf  21855  islindf4  21881  psrmulfval  21986  evlslem2  22126  evlslem3  22127  evlslem1  22129  mpfrcl  22132  selvval  22162  psdval  22186  psdcoef  22187  psdadd  22190  psdmul  22193  coe1fval  22228  coe1mul2lem2  22292  coe1tm  22297  madetsumid  22488  mvmulval  22570  marepvval0  22593  mulmarep1gsum2  22601  mdetleib2  22615  m1detdiag  22624  mdetralt  22635  mdetunilem7  22645  mdetunilem9  22647  m2detleiblem3  22656  m2detleiblem4  22657  m2detleib  22658  symgmatr01lem  22680  gsummatr01lem1  22682  gsummatr01lem4  22685  gsummatr01  22686  smadiadetlem3  22695  pmatcoe1fsupp  22728  pmatcollpw3lem  22810  pmatcollpw3fi1lem2  22814  iscnp  23266  1stcfb  23474  ptpjpre1  23600  elpt  23601  elptr  23602  ptpjopn  23641  dfac14  23647  upxp  23652  pthaus  23667  ptrescn  23668  xkoptsub  23683  cnmptkp  23709  xkofvcn  23713  cnmptk1p  23714  cnmptk2  23715  ptunhmeo  23837  ptcmplem3  24083  ptcmplem4  24084  symgtgp  24135  prdstmdd  24153  isucn  24308  imasdsf1olem  24404  prdsxmslem2  24563  tngngp3  24698  nmoval  24757  elcncf  24934  ishtpy  25023  pcoval  25063  om1elbas  25084  elpi1i  25098  iscau  25329  rrxds  25446  rrxdsfival  25466  ehl1eudisval  25474  ehl2eudisval  25476  mbfi1fseqlem6  25775  mbfi1flimlem  25777  isibl  25820  deg1ldg  26151  deg1leb  26154  elply2  26255  elplyr  26260  ne0p  26266  coeeu  26284  coelem  26285  coeeq  26286  coeidlem  26296  elqaalem3  26381  qaa  26383  iaa  26385  aareccl  26386  aannenlem2  26389  aaliou2  26400  dchrptlem2  27327  dchrpt  27329  dchrsum2  27330  sumdchr2  27332  dchrvmaeq0  27566  rpvmasum2  27574  dchrisum0re  27575  ostth  27701  sltval  27710  nolesgn2o  27734  nogesgn1o  27736  noresle  27760  nosupprefixmo  27763  noinfprefixmo  27764  nosupcbv  27765  nosupfv  27769  noinfcbv  27780  noinffv  27784  iscgrg  28538  isismt  28560  israg  28723  iseqlg  28893  brbtwn  28932  brbtwn2  28938  colinearalg  28943  axsegconlem1  28950  axsegcon  28960  ax5seglem5  28966  axpasch  28974  axlowdim  28994  axeuclidlem  28995  axcontlem1  28997  axcontlem2  28998  axcontlem5  29001  vtxdgfval  29503  1egrvtxdg1  29545  isewlk  29638  iswlk  29646  uspgr2wlkeq2  29683  iswlkon  29693  isclwlk  29809  iscrct  29826  iscycl  29827  iswwlks  29869  wwlknon  29890  wlkiswwlks2  29908  wwlksnredwwlkn0  29929  wlksnwwlknvbij  29941  wwlksnextproplem3  29944  wwlksnextprop  29945  umgr2wlk  29982  midwwlks2s3  29985  elwwlks2  29999  elwspths2spth  30000  rusgrnumwwlkslem  30002  rusgrnumwwlkb0  30004  rusgrnumwwlks  30007  isclwwlk  30016  clwlkclwwlklem1  30031  clwwlkn1loopb  30075  clwwlkel  30078  clwwlkf  30079  clwwlkf1  30081  isclwwlknon  30123  clwwlknon1  30129  s2elclwwlknon2  30136  clwwlkvbij  30145  uhgr3cyclex  30214  fusgreg2wsplem  30365  fusgr2wsp2nb  30366  fusgreghash2wsp  30370  2clwwlkel  30381  extwwlkfabel  30385  numclwwlk1lem2fv  30388  numclwwlk1lem2  30392  clwwlknonclwlknonf1o  30394  dlwwlknondlwlknonf1o  30397  numclwwlk2lem1  30408  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  ex-fv  30475  isnvlem  30642  islno  30785  nmooval  30795  nmblolbi  30832  isphg  30849  ajmoi  30890  ajval  30893  ubthlem3  30904  htthlem  30949  hcau  31216  hlimi  31220  hosmval  31767  hommval  31768  hodmval  31769  hfsmval  31770  hfmmval  31771  adjmo  31864  nmopval  31888  elcnop  31889  ellnop  31890  elunop  31904  elhmop  31905  nmfnval  31908  elcnfn  31914  ellnfn  31915  adjeu  31921  adjval  31922  eigvecval  31928  eigvalfval  31929  adj1  31965  adjeq  31967  hmopadj2  31973  lnopeq0i  32039  lnopeq  32041  elunop2  32045  lnophm  32051  hmopco  32055  nmbdoplb  32057  nmcoplb  32062  lnopcon  32067  lnfn0  32079  lnfnmul  32080  nmbdfnlb  32082  nmcfnlb  32086  lnfncon  32088  riesz4  32096  riesz1  32097  cnlnadjlem9  32107  cnlnadjeu  32110  cnlnssadj  32112  nmopcoi  32127  bra11  32140  cnvbraval  32142  pjss2coi  32196  pjssdif2i  32206  pjssdif1i  32207  pjclem4  32231  pj3si  32239  pj3cor1i  32241  isst  32245  ishst  32246  stri  32289  hstri  32297  aciunf1lem  32680  ismnt  32956  mgcval  32960  ischn  32979  chnind  32983  chnub  32984  fzo0pmtrlast  33085  linds2eq  33374  elrspunidl  33421  elrspunsn  33422  dfufd2lem  33542  lbsdiflsp0  33639  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  fldext2chn  33719  lmatval  33759  mdetpmtr1  33769  zarcmplem  33827  ismeas  34163  isrnmeas  34164  cntnevol  34192  carsgval  34268  sitgval  34297  eulerpartleme  34328  eulerpartlemd  34331  eulerpartlemr  34339  eulerpartlemgvv  34341  eulerpart  34347  cndprobval  34398  signstfvneq0  34549  reprsum  34590  reprsuc  34592  reprpmtf1o  34603  reprdifc  34604  breprexp  34610  vtsval  34614  hgt750lemb  34633  hgt750lema  34634  hgt750leme  34635  bnj66  34836  bnj106  34844  bnj125  34848  bnj154  34854  bnj155  34855  bnj526  34864  bnj540  34868  bnj609  34893  bnj611  34894  bnj893  34904  bnj1000  34917  bnj1014  34937  bnj1015  34938  bnj1234  34989  bnj1463  35031  gblacfnacd  35075  loop1cycl  35105  derangenlem  35139  subfacp1lem3  35150  subfacp1lem5  35152  subfacp1lem6  35153  subfacp1  35154  sconnpht  35197  cnpconn  35198  txpconn  35200  ptpconn  35201  indispconn  35202  connpconn  35203  cvxpconn  35210  cvmliftmo  35252  cvmliftlem14  35265  cvmliftlem15  35266  cvmliftiota  35269  cvmlift2  35284  cvmliftphtlem  35285  cvmlift3lem2  35288  cvmlift3lem6  35292  cvmlift3lem7  35293  cvmlift3lem9  35295  cvmlift3  35296  satfv1lem  35330  satfv1  35331  sategoelfvb  35387  mrsubff1  35482  mrsub0  35484  mrsubccat  35486  mrsubcn  35487  elmsubrn  35496  msubrn  35497  msubco  35499  msubvrs  35528  mclsax  35537  shftvalg  35694  fwddifval  36126  fwddifnval  36127  bj-evalval  37041  unceq  37557  matunitlindflem2  37577  poimirlem17  37597  poimirlem20  37600  poimirlem22  37602  poimirlem23  37603  poimirlem27  37607  poimirlem28  37608  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  poimir  37613  broucube  37614  voliunnfl  37624  volsupnfl  37625  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  ftc1anclem2  37654  ftc1anclem5  37657  upixp  37689  fdc  37705  isismty  37761  rrnmval  37788  elghomlem2OLD  37846  isrngohom  37925  islfl  39016  isopos  39136  islaut  40040  ispautN  40056  isldil  40067  isltrn  40076  ltrnid  40092  ltrneq2  40105  isdilN  40111  istrnN  40114  trlval  40119  ltrneq3  40165  cdleme50ex  40516  cdleme  40517  cdlemg1a  40527  ltrniotaval  40538  ltrniotavalbN  40541  cdlemeiota  40542  cdlemg2jlemOLDN  40550  cdlemg2fvlem  40551  cdlemg2klem  40552  istendo  40717  tendoplcbv  40732  tendopl  40733  tendoicbv  40750  tendoi  40751  tendoid0  40782  tendo1ne0  40785  cdlemksv2  40804  cdlemkuv2  40824  cdlemk33N  40866  cdlemk34  40867  cdlemk36  40870  cdlemk19u  40927  cdlemk  40931  tendoex  40932  dvavsca  40974  dvhvscacbv  41055  dvhvscaval  41056  dicopelval  41134  dicelval1sta  41144  diclspsn  41151  dihmeetlem13N  41276  dih1dimatlem0  41285  dih1dimatlem  41286  dihpN  41293  islpolN  41440  hdmap1fval  41753  hdmapfval  41784  sticksstones1  42103  sticksstones2  42104  sticksstones3  42105  sticksstones8  42110  sticksstones10  42112  sticksstones11  42113  sticksstones12a  42114  sticksstones12  42115  sticksstones15  42118  frlmsnic  42495  uvcn0  42497  pwsgprod  42499  mplmapghm  42511  evlsvval  42515  evlsvvval  42518  evlsvarval  42520  evlsbagval  42521  selvvvval  42540  evlselv  42542  fsuppssindlem2  42547  fsuppssind  42548  prjspnfv01  42579  prjspner01  42580  prjspner1  42581  sn-isghm  42628  ismrc  42657  mzpclval  42681  mzpsubst  42704  mzprename  42705  mzpcompact2lem  42707  eldioph  42714  eldioph2  42718  eldioph2b  42719  eldioph3  42722  rexrabdioph  42750  2rexfrabdioph  42752  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  eldioph4i  42768  rabren3dioph  42771  mzpcong  42929  jm2.27dlem1  42966  wepwsolem  42999  aomclem6  43016  aomclem8  43018  dfac11  43019  dgraalem  43102  dgraaub  43105  dgraa0p  43106  mpaaeu  43107  mpaalem  43109  aaitgo  43119  rngunsnply  43130  cantnfresb  43286  tfsconcatun  43299  nvocnvb  43384  eliunov2  43641  rfovcnvfvd  43969  fsovfvd  43972  fsovcnvlem  43975  dssmapfv2d  43980  dssmapnvod  43982  clsk1independent  44008  ntrclskb  44031  ntrclsk13  44033  gneispace2  44094  mnringmulrvald  44196  dvconstbi  44303  addrval  44435  subrval  44436  mulvval  44437  fnchoice  44929  refsum2cnlem1  44937  choicefi  45107  axccdom  45129  fmulcl  45502  fmuldfeqlem1  45503  mccllem  45518  mccl  45519  climf  45543  climf2  45587  dvnprodlem1  45867  dvnprodlem3  45869  dvnprod  45870  stoweidlem2  45923  stoweidlem6  45927  stoweidlem8  45929  stoweidlem9  45930  stoweidlem15  45936  stoweidlem16  45937  stoweidlem17  45938  stoweidlem18  45939  stoweidlem21  45942  stoweidlem27  45948  stoweidlem31  45952  stoweidlem36  45957  stoweidlem37  45958  stoweidlem41  45962  stoweidlem43  45964  stoweidlem44  45965  stoweidlem45  45966  stoweidlem46  45967  stoweidlem48  45969  stoweidlem51  45972  stoweidlem55  45976  stoweidlem59  45980  stoweidlem60  45981  stoweidlem62  45983  fourierdlem2  46030  fourierdlem3  46031  elaa2lem  46154  etransclem11  46166  etransclem24  46179  etransclem26  46181  etransclem28  46183  etransclem35  46190  rrndistlt  46211  ioorrnopn  46226  subsaliuncllem  46278  sge0val  46287  ismea  46372  caragenval  46414  isome  46415  isomenndlem  46451  hoicvrrex  46477  ovnlecvr  46479  ovncvrrp  46485  ovn0lem  46486  ovnsubaddlem1  46491  ovnsubadd  46493  hsphoif  46497  hoidmvval  46498  hsphoival  46500  hoidmvlelem3  46518  hoidmvlelem5  46520  hoidmvle  46521  ovnhoilem1  46522  ovnhoi  46524  ovnlecvr2  46531  ovncvr2  46532  hoidifhspval2  46536  hoiqssbllem2  46544  hspmbllem2  46548  hspmbllem3  46549  hspmbl  46550  ovnovollem1  46577  smfmullem2  46713  smfmul  46716  smfpimcclem  46728  tworepnotupword  46805  cfsetsnfsetfv  46972  cfsetsnfsetfo  46975  iccpart  47290  iccpartiun  47308  icceuelpart  47310  nnsum3primes4  47662  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbtbnd  47683  isisubgr  47734  isgrim  47752  isuspgrim0  47756  grimidvtxedg  47760  grimcnv  47763  grimco  47764  gricushgr  47770  ushggricedg  47780  uhgrimisgrgric  47783  isgrtri  47794  isgrlim  47806  uspgrlim  47816  grlicref  47829  grlicsym  47830  grlictr  47832  isupwlk  47859  lincval  48138  lincdifsn  48153  linindslinci  48177  lindslinindsimp1  48186  linds0  48194  el0ldep  48195  lindsrng01  48197  snlindsntorlem  48199  ldepspr  48202  islindeps2  48212  zlmodzxzldep  48233  bigoval  48283  elbigo  48285  0aryfvalelfv  48369  1arympt1fv  48373  1arymaptfv  48374  1arymaptfo  48377  2arymptfv  48384  2arymaptfv  48385  2arymaptfo  48388  prelrrx2b  48448  rrx2plord  48454  rrx2vlinest  48475  rrx2linesl  48477  elrrx2linest2  48479  line2ylem  48485  line2xlem  48487  itsclc0  48505  itsclc0b  48506  itscnhlinecirc02p  48519  elfvne0  48562  thincciso  48716  setrecseq  48777  aacllem  48895