MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fveq12d Structured version   Visualization version   GIF version

Theorem fveq12d 6849
Description: Equality deduction for function value. (Contributed by FL, 22-Dec-2008.)
Hypotheses
Ref Expression
fveq12d.1 (𝜑𝐹 = 𝐺)
fveq12d.2 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
fveq12d (𝜑 → (𝐹𝐴) = (𝐺𝐵))

Proof of Theorem fveq12d
StepHypRef Expression
1 fveq12d.1 . . 3 (𝜑𝐹 = 𝐺)
21fveq1d 6844 . 2 (𝜑 → (𝐹𝐴) = (𝐺𝐴))
3 fveq12d.2 . . 3 (𝜑𝐴 = 𝐵)
43fveq2d 6846 . 2 (𝜑 → (𝐺𝐴) = (𝐺𝐵))
52, 4eqtrd 2776 1 (𝜑 → (𝐹𝐴) = (𝐺𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  cfv 6496
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504
This theorem is referenced by:  nffvd  6854  fvmpopr2d  7515  wrecseq123OLD  8245  tfrlem3a  8322  resixpfo  8873  cantnfval  9603  cantnfres  9612  fseqenlem1  9959  fseqenlem2  9960  dfac12lem1  10078  dfac12lem2  10079  dfac12r  10081  hsmexlem2  10362  ttukeylem3  10446  ttukey2g  10451  seq1  13918  expval  13968  lsw  14451  ccatfval  14460  swrdval  14530  splfv2a  14643  revval  14647  relexpsucnnr  14909  relexp1g  14910  seqshft  14969  climshft2  15463  fprodser  15831  imasval  17392  funcid  17755  funcco  17756  funcoppc  17760  funcres  17781  nati  17841  funcestrcsetclem7  18033  funcestrcsetclem9  18035  funcsetcestrclem7  18048  funcsetcestrclem9  18050  evlf2  18106  evlf1  18108  evlfcl  18110  uncf2  18125  hofcl  18147  yonedalem21  18161  yonedalem3a  18162  yonedalem4a  18163  yonedalem4b  18164  yonedalem22  18166  yonedalem3  18168  yonedainv  18169  p0val  18315  p1val  18316  gsumvalx  18530  gsumpropd  18532  gsumval2a  18539  gsumsgrpccat  18649  prdsinvlem  18854  mulgfval  18872  mulgfvalALT  18873  mulgval  18874  mulgnndir  18903  mulgpropd  18916  cntrval  19097  efgsf  19509  efgsval  19511  issrngd  20318  rlmval  20658  chrval  20926  znval  20936  isphl  21030  isphld  21056  phlpropd  21057  cssval  21084  prdsinvgd2  21146  islindf  21216  evlseu  21491  evlval  21503  selvffval  21524  selvval  21526  evls1fval  21683  evl1varpw  21725  madetsumid  21808  madufval  21984  smadiadetr  22022  decpmatval0  22111  chpmatfval  22177  isperf  22500  dfac14  22967  xkohmeo  23164  flffval  23338  fcfval  23382  cnextfval  23411  tsmsval2  23479  tsmspropd  23481  tngngp  24016  tngngp3  24018  isnlm  24037  sranlm  24046  cnncvsabsnegdemo  24527  ovoliunlem1  24864  ovoliunlem2  24865  limcfval  25234  dvfval  25259  dvreslem  25271  dvaddbr  25300  dvmulbr  25301  isuc1p  25503  ismon1p  25505  q1pval  25516  dgreq0  25624  vieta1lem2  25669  vieta1  25670  basellem5  26432  lgsval  26647  lgsneg  26667  israg  27586  iswlkon  28552  wlkres  28565  wlkp1lem3  28570  wlkp1lem6  28573  isclwlk  28668  iscrct  28685  iscycl  28686  eupth2eucrct  29108  dipfval  29591  splfv3  31756  cycpmco2lem5  31923  cycpmco2lem6  31924  idlsrgval  32185  extdgval  32283  minplyval  32312  lmatfval  32335  lmat22e11  32339  rrhval  32517  xrhval  32539  prodindf  32562  brae  32780  braew  32781  sitmval  32889  sseqval  32928  fibp1  32941  elprob  32949  signsvtn0  33122  signstfvneq0  33124  signstfveq0  33129  breprexplema  33183  breprexp  33186  circlevma  33195  circlemethhgt  33196  cvmliftlem5  33823  cvmliftlem7  33825  cvmliftlem10  33828  cvmliftlem13  33830  satefv  33948  mclsval  34097  rdgprc0  34308  dfrdg2  34310  bj-finsumval0  35746  rdgeqoa  35831  finxpeq2  35848  finxpreclem6  35857  finxpsuclem  35858  sdclem2  36191  ldualvsub  37607  ldualvsubval  37609  isopos  37632  polfvalN  38357  psubclsetN  38389  docaffvalN  39574  docafvalN  39575  djaffvalN  39586  djafvalN  39587  dihffval  39683  dihfval  39684  dochffval  39802  dochfval  39803  djhffval  39849  djhfval  39850  islpolN  39936  lcdfval  40041  lcdval  40042  lcdvsub  40070  lcdvsubval  40071  mapdffval  40079  mapdfval  40080  hdmap1fval  40249  hdmapfval  40280  hgmapfval  40339  hdmapglem7  40382  hlhilset  40387  0prjspnrel  40942  ismrc  41001  rmxfval  41204  rmyfval  41205  aomclem8  41365  hbt  41434  elmnc  41440  mncn0  41443  aaitgo  41466  mon1pid  41509  clsk1independent  42299  binomcxp  42618  limciccioolb  43833  limcicciooub  43849  ioccncflimc  44097  icocncflimc  44101  dvnprodlem2  44159  dvnprodlem3  44160  dirkercncflem3  44317  fourierdlem32  44351  etransclem32  44478  etransclem44  44490  etransclem46  44492  etransc  44495  ovnsubaddlem1  44782  ovnsubaddlem2  44783  ovnsubadd  44784  hoidmvlelem4  44810  hoidmvlelem5  44811  hspmbl  44841  vonioo  44894  vonicc  44897  afveq12d  45336  iccelpart  45596  nnsum3primesprm  45953  isomgreqve  45988  funcringcsetcALTV2lem7  46311  funcringcsetcALTV2lem9  46313  funcringcsetclem7ALTV  46334  funcringcsetclem9ALTV  46336
  Copyright terms: Public domain W3C validator