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

Theorem fvconst2g 5924
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 5590 . 2  |-  ( B  e.  D  ->  ( A  X.  { B }
) : A --> { B } )
2 fvconst 5890 . 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 1369    e. wcel 1756   {csn 3870    X. cxp 4830   -->wf 5407   ` cfv 5411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-sep 4406  ax-nul 4414  ax-pr 4524
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-opab 4344  df-mpt 4345  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-fv 5419
This theorem is referenced by:  fconst2g  5925  fvconst2  5926  fnsuppresOLD  5931  ofc1  6338  ofc2  6339  caofid0l  6343  caofid0r  6344  caofid1  6345  caofid2  6346  fnsuppres  6711  ser0  11850  ser1const  11854  exp1  11863  expp1  11864  climconst2  13018  climaddc1  13104  climmulc2  13106  climsubc1  13107  climsubc2  13108  climlec2  13128  fsumconst  13249  supcvg  13310  seq1st  13738  algr0  13739  algrf  13740  ramz  14078  pwsbas  14417  pwsplusgval  14420  pwsmulrval  14421  pwsle  14422  pwsvscafval  14424  pwspjmhm  15487  pwsco1mhm  15489  mulg1  15623  mulgnnp1  15624  mulgnnsubcl  15628  mulgnn0z  15636  mulgnndir  15638  pwsinvg  15656  mulgnn0di  16302  gsumconst  16415  pwslmod  17025  psrlidm  17448  psrlidmOLD  17449  psrridmOLD  17451  coe1tm  17697  evl1scad  17738  frlmvscaval  18163  frlmip  18172  lmconst  18834  cnconst2  18856  xkoptsub  19196  xkopt  19197  xkopjcn  19198  tmdgsum  19635  tmdgsum2  19636  symgtgp  19641  cstucnd  19828  pcoptcl  20562  pcopt  20563  pcopt2  20564  rrxip  20863  dvidlem  21359  dvconst  21360  dvnff  21366  dvn0  21367  dvcmul  21387  dvcmulf  21388  fta1blem  21609  plyeq0lem  21647  coemulc  21691  dgreq0  21701  dgrmulc  21707  qaa  21758  dchrisumlema  22706  gx1  23694  gxnn0suc  23696  ofcc  26496  ofcof  26497  sseqf  26723  sseqp1  26726  cvmlift3lem9  27164  prodf1  27353  prod0  27403  fprodconst  27436  ismrer1  28680  stoweidlem21  29759  stoweidlem47  29785  zlmodzxzscm  30689
  Copyright terms: Public domain W3C validator