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

Theorem fvconst2 6079
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 6077 . 2  |-  ( ( B  e.  _V  /\  C  e.  A )  ->  ( ( A  X.  { B } ) `  C )  =  B )
31, 2mpan 674 1  |-  ( C  e.  A  ->  (
( A  X.  { B } ) `  C
)  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1872   _Vcvv 3022   {csn 3941    X. cxp 4794   ` cfv 5544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-fv 5552
This theorem is referenced by:  ovconst2  6407  mapsncnv  7473  ofsubeq0  10557  ofsubge0  10559  ser0f  12216  hashinf  12470  iserge0  13667  iseraltlem1  13691  sum0  13730  sumz  13731  harmonic  13860  prodf1f  13891  fprodntriv  13939  prod1  13941  setcmon  15925  0mhm  16548  mulgpropd  16734  dprdsubg  17600  0lmhm  18206  mplsubglem  18601  coe1tm  18809  frlmlmod  19254  frlmlss  19256  frlmbas  19260  frlmip  19278  islindf4  19338  mdetuni0  19588  txkgen  20609  xkofvcn  20641  nmo0  21698  pcorevlem  21999  rrxip  22291  mbfpos  22549  0pval  22571  0pledm  22573  xrge0f  22631  itg2ge0  22635  ibl0  22686  bddibl  22739  dvcmul  22840  dvef  22874  rolle  22884  dveq0  22894  dv11cn  22895  ftc2  22938  tdeglem4  22951  ply1rem  23056  fta1g  23060  fta1blem  23061  0dgrb  23142  dgrnznn  23143  dgrlt  23162  plymul0or  23176  plydivlem4  23191  plyrem  23200  fta1  23203  vieta1lem2  23206  elqaalem3  23216  elqaalem3OLD  23219  aaliou2  23238  ulmdvlem1  23297  dchrelbas2  24107  dchrisumlem3  24271  axlowdimlem9  24922  axlowdimlem12  24925  axlowdimlem17  24930  0oval  26371  occllem  26898  ho01i  27423  0cnfn  27575  0lnfn  27580  nmfn0  27582  nlelchi  27656  opsqrlem2  27736  opsqrlem4  27738  opsqrlem5  27739  hmopidmchi  27746  conpcon  29910  txsconlem  29915  cvxscon  29918  cvmliftphtlem  29992  nobndlem7  30536  nobndup  30538  nobnddown  30539  fullfunfv  30663  ptrecube  31847  poimirlem1  31848  poimirlem2  31849  poimirlem3  31850  poimirlem4  31851  poimirlem5  31852  poimirlem6  31853  poimirlem7  31854  poimirlem10  31857  poimirlem11  31858  poimirlem12  31859  poimirlem16  31863  poimirlem17  31864  poimirlem19  31866  poimirlem20  31867  poimirlem22  31869  poimirlem23  31870  poimirlem28  31875  poimirlem29  31876  poimirlem30  31877  poimirlem31  31878  poimirlem32  31879  poimir  31880  broucube  31881  mblfinlem2  31885  itg2addnclem  31900  itg2addnc  31903  ftc1anclem5  31928  ftc2nc  31933  cnpwstotbnd  32036  lfl0f  32547  eqlkr2  32578  lcd0vvalN  35093  mzpsubst  35502  mzpcompact2lem  35505  mzpcong  35735  hbtlem2  35896  mncn0  35911  mpaaeu  35929  aaitgo  35941  rngunsnply  35952  hashnzfzclim  36584  ofsubid  36586  dvconstbi  36596  binomcxplemnotnn0  36618  n0p  37292  aacllem  40143
  Copyright terms: Public domain W3C validator