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

Theorem fvconst2g 6109
Description: The value of a constant function. (Contributed by NM, 20-Aug-2005.)
Assertion
Ref Expression
fvconst2g  |-  ( ( B  e.  D  /\  C  e.  A )  ->  ( ( A  X.  { B } ) `  C )  =  B )

Proof of Theorem fvconst2g
StepHypRef Expression
1 fconstg 5762 . 2  |-  ( B  e.  D  ->  ( A  X.  { B }
) : A --> { B } )
2 fvconst 6074 . 2  |-  ( ( ( A  X.  { B } ) : A --> { B }  /\  C  e.  A )  ->  (
( A  X.  { B } ) `  C
)  =  B )
31, 2sylan 471 1  |-  ( ( B  e.  D  /\  C  e.  A )  ->  ( ( A  X.  { B } ) `  C )  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1383    e. wcel 1804   {csn 4014    X. cxp 4987   -->wf 5574   ` cfv 5578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-fv 5586
This theorem is referenced by:  fconst2g  6110  fvconst2  6111  fnsuppresOLD  6116  ofc1  6548  ofc2  6549  caofid0l  6553  caofid0r  6554  caofid1  6555  caofid2  6556  fnsuppres  6929  ser0  12138  ser1const  12142  exp1  12151  expp1  12152  climconst2  13350  climaddc1  13436  climmulc2  13438  climsubc1  13439  climsubc2  13440  climlec2  13460  fsumconst  13584  supcvg  13646  seq1st  14077  algr0  14078  algrf  14079  ramz  14420  pwsbas  14761  pwsplusgval  14764  pwsmulrval  14765  pwsle  14766  pwsvscafval  14768  pwspjmhm  15873  pwsco1mhm  15875  mulg1  16023  mulgnnp1  16024  mulgnnsubcl  16028  mulgnn0z  16036  mulgnndir  16038  pwsinvg  16056  mulgnn0di  16708  gsumconst  16828  pwslmod  17490  psrlidm  17930  psrlidmOLD  17931  psrridmOLD  17933  coe1tm  18188  coe1fzgsumd  18218  evl1scad  18245  frlmvscaval  18673  decpmatid  19144  pmatcollpwscmatlem1  19163  lmconst  19635  cnconst2  19657  xkoptsub  20028  xkopt  20029  xkopjcn  20030  tmdgsum  20467  tmdgsum2  20468  symgtgp  20473  cstucnd  20660  pcoptcl  21394  pcopt  21395  pcopt2  21396  dvidlem  22192  dvconst  22193  dvnff  22199  dvn0  22200  dvcmul  22220  dvcmulf  22221  fta1blem  22442  plyeq0lem  22480  coemulc  22524  dgreq0  22534  dgrmulc  22540  qaa  22591  dchrisumlema  23545  gx1  25136  gxnn0suc  25138  ofcc  27978  ofcof  27979  sseqf  28204  sseqp1  28207  cvmlift3lem9  28645  prodf1  29000  prod0  29050  fprodconst  29083  ismrer1  30309  dvsinax  31612  stoweidlem21  31692  stoweidlem47  31718  zlmodzxzscm  32679
  Copyright terms: Public domain W3C validator