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

Theorem fvconst2 6939
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 6937 . 2 ((𝐵 ∈ V ∧ 𝐶𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
31, 2mpan 689 1 (𝐶𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  Vcvv 3471  {csn 4540   × cxp 5526  cfv 6328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pr 5303
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-sbc 3750  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-mpt 5120  df-id 5433  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-fv 6336
This theorem is referenced by:  ovconst2  7303  mapsncnv  8432  ofsubeq0  11612  ofsubge0  11614  ser0f  13407  hashinf  13679  iserge0  14996  iseraltlem1  15017  sum0  15057  sumz  15058  harmonic  15193  prodf1f  15227  fprodntriv  15275  prod1  15277  setcmon  17325  0mhm  17962  mulgfval  18204  mulgpropd  18247  dprdsubg  19124  0lmhm  19787  mplsubglem  20189  coe1tm  20416  frlmlmod  20868  frlmlss  20870  frlmbas  20874  frlmip  20897  islindf4  20957  mdetuni0  21205  txkgen  22235  xkofvcn  22267  nmo0  23319  pcorevlem  23609  rrxip  23972  mbfpos  24233  0pval  24253  0pledm  24255  xrge0f  24313  itg2ge0  24317  ibl0  24368  bddibl  24421  dvcmul  24525  dvef  24561  rolle  24571  dveq0  24581  dv11cn  24582  ftc2  24625  tdeglem4  24639  ply1rem  24742  fta1g  24746  fta1blem  24747  0dgrb  24821  dgrnznn  24822  dgrlt  24841  plymul0or  24855  plydivlem4  24870  plyrem  24879  fta1  24882  vieta1lem2  24885  elqaalem3  24895  aaliou2  24914  ulmdvlem1  24973  dchrelbas2  25799  dchrisumlem3  26053  axlowdimlem9  26722  axlowdimlem12  26725  axlowdimlem17  26730  0oval  28549  occllem  29064  ho01i  29589  0cnfn  29741  0lnfn  29746  nmfn0  29748  nlelchi  29822  opsqrlem2  29902  opsqrlem4  29904  opsqrlem5  29905  hmopidmchi  29912  lbsdiflsp0  31032  breprexpnat  31912  circlemethnat  31919  circlevma  31920  connpconn  32489  txsconnlem  32494  cvxsconn  32497  cvmliftphtlem  32571  noetalem3  33226  fullfunfv  33415  matunitlindflem1  34931  matunitlindflem2  34932  ptrecube  34935  poimirlem1  34936  poimirlem2  34937  poimirlem3  34938  poimirlem4  34939  poimirlem5  34940  poimirlem6  34941  poimirlem7  34942  poimirlem10  34945  poimirlem11  34946  poimirlem12  34947  poimirlem16  34951  poimirlem17  34952  poimirlem19  34954  poimirlem20  34955  poimirlem22  34957  poimirlem23  34958  poimirlem28  34963  poimirlem29  34964  poimirlem30  34965  poimirlem31  34966  poimirlem32  34967  poimir  34968  broucube  34969  mblfinlem2  34973  itg2addnclem  34986  itg2addnc  34989  ftc1anclem5  35012  ftc2nc  35017  cnpwstotbnd  35113  lfl0f  36243  eqlkr2  36274  lcd0vvalN  38787  uvcn0  39273  mzpsubst  39484  mzpcompact2lem  39487  mzpcong  39708  hbtlem2  39863  mncn0  39878  mpaaeu  39889  aaitgo  39901  rngunsnply  39912  hashnzfzclim  40809  ofsubid  40811  dvconstbi  40821  binomcxplemnotnn0  40843  n0p  41460  snelmap  41501  aacllem  45089
  Copyright terms: Public domain W3C validator