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

Theorem fvconst2 6352
Description: The value of a constant function. (Contributed by NM, 16-Apr-2005.)
Hypothesis
Ref Expression
fvconst2.1 𝐵 ∈ V
Assertion
Ref Expression
fvconst2 (𝐶𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Proof of Theorem fvconst2
StepHypRef Expression
1 fvconst2.1 . 2 𝐵 ∈ V
2 fvconst2g 6350 . 2 ((𝐵 ∈ V ∧ 𝐶𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
31, 2mpan 701 1 (𝐶𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  Vcvv 3172  {csn 4124   × cxp 5026  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-fv 5798
This theorem is referenced by:  ovconst2  6689  mapsncnv  7767  ofsubeq0  10864  ofsubge0  10866  ser0f  12671  hashinf  12939  iserge0  14185  iseraltlem1  14206  sum0  14245  sumz  14246  harmonic  14376  prodf1f  14409  fprodntriv  14457  prod1  14459  setcmon  16506  0mhm  17127  mulgpropd  17353  dprdsubg  18192  0lmhm  18807  mplsubglem  19201  coe1tm  19410  frlmlmod  19854  frlmlss  19856  frlmbas  19860  frlmip  19878  islindf4  19938  mdetuni0  20188  txkgen  21207  xkofvcn  21239  nmo0  22281  pcorevlem  22565  rrxip  22903  mbfpos  23141  0pval  23161  0pledm  23163  xrge0f  23221  itg2ge0  23225  ibl0  23276  bddibl  23329  dvcmul  23430  dvef  23464  rolle  23474  dveq0  23484  dv11cn  23485  ftc2  23528  tdeglem4  23541  ply1rem  23644  fta1g  23648  fta1blem  23649  0dgrb  23723  dgrnznn  23724  dgrlt  23743  plymul0or  23757  plydivlem4  23772  plyrem  23781  fta1  23784  vieta1lem2  23787  elqaalem3  23797  aaliou2  23816  ulmdvlem1  23875  dchrelbas2  24679  dchrisumlem3  24897  axlowdimlem9  25548  axlowdimlem12  25551  axlowdimlem17  25556  0oval  26833  occllem  27352  ho01i  27877  0cnfn  28029  0lnfn  28034  nmfn0  28036  nlelchi  28110  opsqrlem2  28190  opsqrlem4  28192  opsqrlem5  28193  hmopidmchi  28200  conpcon  30277  txsconlem  30282  cvxscon  30285  cvmliftphtlem  30359  nobndlem7  30903  nobndup  30905  nobnddown  30906  fullfunfv  31030  matunitlindflem1  32378  matunitlindflem2  32379  ptrecube  32382  poimirlem1  32383  poimirlem2  32384  poimirlem3  32385  poimirlem4  32386  poimirlem5  32387  poimirlem6  32388  poimirlem7  32389  poimirlem10  32392  poimirlem11  32393  poimirlem12  32394  poimirlem16  32398  poimirlem17  32399  poimirlem19  32401  poimirlem20  32402  poimirlem22  32404  poimirlem23  32405  poimirlem28  32410  poimirlem29  32411  poimirlem30  32412  poimirlem31  32413  poimirlem32  32414  poimir  32415  broucube  32416  mblfinlem2  32420  itg2addnclem  32434  itg2addnc  32437  ftc1anclem5  32462  ftc2nc  32467  cnpwstotbnd  32569  lfl0f  33177  eqlkr2  33208  lcd0vvalN  35723  mzpsubst  36132  mzpcompact2lem  36135  mzpcong  36360  hbtlem2  36516  mncn0  36531  mpaaeu  36542  aaitgo  36554  rngunsnply  36565  hashnzfzclim  37346  ofsubid  37348  dvconstbi  37358  binomcxplemnotnn0  37380  n0p  38037  snelmap  38083  aacllem  42319
  Copyright terms: Public domain W3C validator