MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvconst2g Unicode version

Theorem fvconst2g 6124
Description: The value of a constant function. (Contributed by NM, 20-Aug-2005.)
Assertion
Ref Expression
fvconst2g

Proof of Theorem fvconst2g
StepHypRef Expression
1 fconstg 5777 . 2
2 fvconst 6089 . 2
31, 2sylan 471 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  {csn 4029  X.cxp 5002  -->wf 5589  `cfv 5593
This theorem is referenced by:  fconst2g  6125  fvconst2  6126  fnsuppresOLD  6131  ofc1  6563  ofc2  6564  caofid0l  6568  caofid0r  6569  caofid1  6570  caofid2  6571  fnsuppres  6946  ser0  12159  ser1const  12163  exp1  12172  expp1  12173  climconst2  13371  climaddc1  13457  climmulc2  13459  climsubc1  13460  climsubc2  13461  climlec2  13481  fsumconst  13605  supcvg  13667  prodf1  13700  prod0  13750  fprodconst  13782  seq1st  14200  algr0  14201  algrf  14202  ramz  14543  pwsbas  14884  pwsplusgval  14887  pwsmulrval  14888  pwsle  14889  pwsvscafval  14891  pwspjmhm  15999  pwsco1mhm  16001  mulg1  16149  mulgnnp1  16150  mulgnnsubcl  16154  mulgnn0z  16162  mulgnndir  16164  pwsinvg  16182  mulgnn0di  16834  gsumconst  16954  pwslmod  17616  psrlidm  18056  psrlidmOLD  18057  psrridmOLD  18059  coe1tm  18314  coe1fzgsumd  18344  evl1scad  18371  frlmvscaval  18800  decpmatid  19271  pmatcollpwscmatlem1  19290  lmconst  19762  cnconst2  19784  xkoptsub  20155  xkopt  20156  xkopjcn  20157  tmdgsum  20594  tmdgsum2  20595  symgtgp  20600  cstucnd  20787  pcoptcl  21521  pcopt  21522  pcopt2  21523  dvidlem  22319  dvconst  22320  dvnff  22326  dvn0  22327  dvcmul  22347  dvcmulf  22348  fta1blem  22569  plyeq0lem  22607  coemulc  22652  dgreq0  22662  dgrmulc  22668  qaa  22719  dchrisumlema  23673  gx1  25264  gxnn0suc  25266  ofcc  28105  ofcof  28106  sseqf  28331  sseqp1  28334  cvmlift3lem9  28772  ismrer1  30334  dvsinax  31708  stoweidlem21  31803  stoweidlem47  31829  elaa2  32017  zlmodzxzscm  32946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601
  Copyright terms: Public domain W3C validator