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

Theorem fvconst2 6041
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 6039 . 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 1370    e. wcel 1758   _Vcvv 3076   {csn 3984    X. cxp 4945   ` cfv 5525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pr 4638
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-fv 5533
This theorem is referenced by:  ovconst2  6352  mapsncnv  7368  ofsubeq0  10429  ofsubge0  10431  ser0f  11975  hashinf  12224  iserge0  13255  iseraltlem1  13276  sum0  13315  sumz  13316  harmonic  13438  setcmon  15073  0mhm  15604  mulgpropd  15778  dprdsubg  16642  0lmhm  17243  mplsubglem  17633  mplsubglemOLD  17635  coe1tm  17849  frlmlmod  18298  frlmlss  18300  frlmbas  18304  frlmbasOLD  18305  islindf4  18391  mdetuni0  18558  txkgen  19356  xkofvcn  19388  nmo0  20445  pcorevlem  20729  mbfpos  21261  0pval  21281  0pledm  21283  xrge0f  21341  itg2ge0  21345  ibl0  21396  bddibl  21449  dvcmul  21550  dvef  21584  rolle  21594  dveq0  21604  dv11cn  21605  ftc2  21648  tdeglem4  21661  ply1rem  21767  fta1g  21771  fta1blem  21772  0dgrb  21846  dgrlt  21865  plymul0or  21879  plydivlem4  21894  plyrem  21903  fta1  21906  vieta1lem2  21909  elqaalem3  21919  aaliou2  21938  ulmdvlem1  21997  dchrelbas2  22708  dchrisumlem3  22872  axlowdimlem9  23347  axlowdimlem12  23350  axlowdimlem17  23355  0oval  24339  occllem  24857  ho01i  25383  0cnfn  25535  0lnfn  25540  nmfn0  25542  nlelchi  25616  opsqrlem2  25696  opsqrlem4  25698  opsqrlem5  25699  hmopidmchi  25706  conpcon  27267  txsconlem  27272  cvxscon  27275  cvmliftphtlem  27349  prodf1f  27550  fprodntriv  27598  prod1  27600  nobndlem7  27982  nobndup  27984  nobnddown  27985  fullfunfv  28121  mblfinlem2  28576  itg2addnclem  28590  itg2addnc  28593  ftc1anclem5  28618  ftc2nc  28623  cnpwstotbnd  28843  mzpsubst  29232  mzpcompact2lem  29235  mzpcong  29462  hbtlem2  29627  dgrnznn  29639  mncn0  29643  mpaaeu  29654  aaitgo  29666  rngunsnply  29677  ofsubid  29745  dvconstbi  29755  lfl0f  33037  eqlkr2  33068  lcd0vvalN  35581
  Copyright terms: Public domain W3C validator