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

Theorem fvconst2g 5727
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 5428 . 2  |-  ( B  e.  D  ->  ( A  X.  { B }
) : A --> { B } )
2 fvconst 5708 . 2  |-  ( ( ( A  X.  { B } ) : A --> { B }  /\  C  e.  A )  ->  (
( A  X.  { B } ) `  C
)  =  B )
31, 2sylan 457 1  |-  ( ( B  e.  D  /\  C  e.  A )  ->  ( ( A  X.  { B } ) `  C )  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   {csn 3640    X. cxp 4687   -->wf 5251   ` cfv 5255
This theorem is referenced by:  fconst2g  5728  fvconst2  5729  fnsuppres  5732  ofc1  6100  ofc2  6101  caofid0l  6105  caofid0r  6106  caofid1  6107  caofid2  6108  ser0  11098  ser1const  11102  exp1  11109  expp1  11110  climconst2  12022  climaddc1  12108  climmulc2  12110  climsubc1  12111  climsubc2  12112  climlec2  12132  fsumconst  12252  supcvg  12314  seq1st  12741  algr0  12742  algrf  12743  ramz  13072  pwsbas  13386  pwsplusgval  13389  pwsmulrval  13390  pwsle  13391  pwsvscafval  13393  pwspjmhm  14444  pwsco1mhm  14446  mulg1  14574  mulgnnp1  14575  mulgnnsubcl  14579  mulgnn0z  14587  mulgnndir  14589  pwsinvg  14607  mulgnn0di  15125  gsumconst  15209  pwslmod  15727  psrlidm  16148  psrridm  16149  coe1tm  16349  lmconst  16991  cnconst2  17011  xkoptsub  17348  xkopt  17349  xkopjcn  17350  tmdgsum  17778  tmdgsum2  17779  symgtgp  17784  pcoptcl  18519  pcopt  18520  pcopt2  18521  dvidlem  19265  dvconst  19266  dvnff  19272  dvn0  19273  dvcmul  19293  dvcmulf  19294  evl1scad  19414  fta1blem  19554  plyeq0lem  19592  coemulc  19636  dgreq0  19646  dgrmulc  19652  qaa  19703  dchrisumlema  20637  gx1  20929  gxnn0suc  20931  ofcc  23467  cvmlift3lem9  23858  ismrer1  26562  frlmvscaval  27231  stoweidlem21  27770  stoweidlem47  27796
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263
  Copyright terms: Public domain W3C validator