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

Theorem fvconst2 5920
Description: The value of a constant function. (Contributed by NM, 16-Apr-2005.)
Hypothesis
Ref Expression
fvconst2.1  |-  B  e. 
_V
Assertion
Ref Expression
fvconst2  |-  ( C  e.  A  ->  (
( A  X.  { B } ) `  C
)  =  B )

Proof of Theorem fvconst2
StepHypRef Expression
1 fvconst2.1 . 2  |-  B  e. 
_V
2 fvconst2g 5918 . 2  |-  ( ( B  e.  _V  /\  C  e.  A )  ->  ( ( A  X.  { B } ) `  C )  =  B )
31, 2mpan 663 1  |-  ( C  e.  A  ->  (
( A  X.  { B } ) `  C
)  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    e. wcel 1755   _Vcvv 2962   {csn 3865    X. cxp 4825   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-fv 5414
This theorem is referenced by:  ovconst2  6232  mapsncnv  7247  ofsubeq0  10307  ofsubge0  10309  ser0f  11843  hashinf  12092  iserge0  13122  iseraltlem1  13143  sum0  13182  sumz  13183  harmonic  13304  setcmon  14938  0mhm  15468  mulgpropd  15640  dprdsubg  16495  0lmhm  17043  mplsubglem  17444  mplsubglemOLD  17446  coe1tm  17624  frlmlmod  18016  frlmlss  18018  frlmbas  18022  frlmbasOLD  18023  islindf4  18109  mdetuni0  18269  txkgen  19067  xkofvcn  19099  nmo0  20156  pcorevlem  20440  mbfpos  20971  0pval  20991  0pledm  20993  xrge0f  21051  itg2ge0  21055  ibl0  21106  bddibl  21159  dvcmul  21260  dvef  21294  rolle  21304  dveq0  21314  dv11cn  21315  ftc2  21358  tdeglem4  21414  ply1rem  21520  fta1g  21524  fta1blem  21525  0dgrb  21599  dgrlt  21618  plymul0or  21632  plydivlem4  21647  plyrem  21656  fta1  21659  vieta1lem2  21662  elqaalem3  21672  aaliou2  21691  ulmdvlem1  21750  dchrelbas2  22461  dchrisumlem3  22625  axlowdimlem9  23019  axlowdimlem12  23022  axlowdimlem17  23027  0oval  24011  occllem  24529  ho01i  25055  0cnfn  25207  0lnfn  25212  nmfn0  25214  nlelchi  25288  opsqrlem2  25368  opsqrlem4  25370  opsqrlem5  25371  hmopidmchi  25378  conpcon  26972  txsconlem  26977  cvxscon  26980  cvmliftphtlem  27054  prodf1f  27254  fprodntriv  27302  prod1  27304  nobndlem7  27686  nobndup  27688  nobnddown  27689  fullfunfv  27825  mblfinlem2  28273  itg2addnclem  28287  itg2addnc  28290  ftc1anclem5  28315  ftc2nc  28320  cnpwstotbnd  28540  mzpsubst  28930  mzpcompact2lem  28933  mzpcong  29160  hbtlem2  29325  dgrnznn  29337  mncn0  29341  mpaaeu  29352  aaitgo  29364  rngunsnply  29375  ofsubid  29443  dvconstbi  29453  lfl0f  32287  eqlkr2  32318  lcd0vvalN  34831
  Copyright terms: Public domain W3C validator