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

Theorem fvconst2 5928
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 5926 . 2  |-  ( ( B  e.  _V  /\  C  e.  A )  ->  ( ( A  X.  { B } ) `  C )  =  B )
31, 2mpan 670 1  |-  ( C  e.  A  ->  (
( A  X.  { B } ) `  C
)  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   _Vcvv 2967   {csn 3872    X. cxp 4833   ` cfv 5413
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 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
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 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421
This theorem is referenced by:  ovconst2  6238  mapsncnv  7251  ofsubeq0  10311  ofsubge0  10313  ser0f  11851  hashinf  12100  iserge0  13130  iseraltlem1  13151  sum0  13190  sumz  13191  harmonic  13313  setcmon  14947  0mhm  15477  mulgpropd  15651  dprdsubg  16509  0lmhm  17098  mplsubglem  17487  mplsubglemOLD  17489  coe1tm  17701  frlmlmod  18149  frlmlss  18151  frlmbas  18155  frlmbasOLD  18156  islindf4  18242  mdetuni0  18402  txkgen  19200  xkofvcn  19232  nmo0  20289  pcorevlem  20573  mbfpos  21104  0pval  21124  0pledm  21126  xrge0f  21184  itg2ge0  21188  ibl0  21239  bddibl  21292  dvcmul  21393  dvef  21427  rolle  21437  dveq0  21447  dv11cn  21448  ftc2  21491  tdeglem4  21504  ply1rem  21610  fta1g  21614  fta1blem  21615  0dgrb  21689  dgrlt  21708  plymul0or  21722  plydivlem4  21737  plyrem  21746  fta1  21749  vieta1lem2  21752  elqaalem3  21762  aaliou2  21781  ulmdvlem1  21840  dchrelbas2  22551  dchrisumlem3  22715  axlowdimlem9  23147  axlowdimlem12  23150  axlowdimlem17  23155  0oval  24139  occllem  24657  ho01i  25183  0cnfn  25335  0lnfn  25340  nmfn0  25342  nlelchi  25416  opsqrlem2  25496  opsqrlem4  25498  opsqrlem5  25499  hmopidmchi  25506  conpcon  27076  txsconlem  27081  cvxscon  27084  cvmliftphtlem  27158  prodf1f  27358  fprodntriv  27406  prod1  27408  nobndlem7  27790  nobndup  27792  nobnddown  27793  fullfunfv  27929  mblfinlem2  28382  itg2addnclem  28396  itg2addnc  28399  ftc1anclem5  28424  ftc2nc  28429  cnpwstotbnd  28649  mzpsubst  29038  mzpcompact2lem  29041  mzpcong  29268  hbtlem2  29433  dgrnznn  29445  mncn0  29449  mpaaeu  29460  aaitgo  29472  rngunsnply  29483  ofsubid  29551  dvconstbi  29561  lfl0f  32554  eqlkr2  32585  lcd0vvalN  35098
  Copyright terms: Public domain W3C validator