Theorem fvconst2 7152

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

Step	Hyp	Ref	Expression
1		fvconst2.1	. 2 ⊢ 𝐵 ∈ V
2		fvconst2g 7150	. 2 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
3	1, 2	mpan 691	1 ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430  {csn 4568   × cxp 5622  ‘cfv 6492

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500

This theorem is referenced by:  ovconst2  7540  mapsncnv  8834  ofsubeq0  12147  ofsubge0  12149  ser0f  14008  hashinf  14288  iserge0  15614  iseraltlem1  15635  sum0  15674  sumz  15675  harmonic  15815  prodf1f  15848  fprodntriv  15898  prod1  15900  setcmon  18045  0mhm  18778  mulgfval  19036  mulgpropd  19083  dprdsubg  19992  pwspjmhmmgpd  20298  0lmhm  21027  frlmlmod  21739  frlmlss  21741  frlmbas  21745  frlmip  21768  islindf4  21828  mplsubglem  21987  evlsvvval  22081  psdmvr  22145  coe1tm  22248  evls1maprnss  22353  mdetuni0  22596  txkgen  23627  xkofvcn  23659  nmo0  24710  pcorevlem  25003  rrxip  25367  mbfpos  25628  0pval  25648  0pledm  25650  xrge0f  25708  itg2ge0  25712  ibl0  25764  bddibl  25817  dvcmul  25921  dvef  25957  rolle  25967  dveq0  25977  dv11cn  25978  ftc2  26021  tdeglem4  26035  ply1rem  26141  fta1g  26145  fta1blem  26146  0dgrb  26221  dgrnznn  26222  dgrlt  26241  plymul0or  26257  plydivlem4  26273  plyrem  26282  fta1  26285  vieta1lem2  26288  elqaalem3  26298  aaliou2  26317  ulmdvlem1  26378  dchrelbas2  27214  dchrisumlem3  27468  noetasuplem4  27714  noetainflem4  27718  axlowdimlem9  29033  axlowdimlem12  29036  axlowdimlem17  29041  0oval  30874  occllem  31389  ho01i  31914  0cnfn  32066  0lnfn  32071  nmfn0  32073  nlelchi  32147  opsqrlem2  32227  opsqrlem4  32229  opsqrlem5  32230  hmopidmchi  32237  elrspunidl  33503  coe1zfv  33665  mplvrpmmhm  33705  vieta  33739  lbsdiflsp0  33786  breprexpnat  34794  circlemethnat  34801  circlevma  34802  connpconn  35433  txsconnlem  35438  cvxsconn  35441  cvmliftphtlem  35515  fullfunfv  36145  matunitlindflem1  37951  matunitlindflem2  37952  ptrecube  37955  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem22  37977  poimirlem23  37978  poimirlem28  37983  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  poimirlem32  37987  poimir  37988  broucube  37989  mblfinlem2  37993  itg2addnclem  38006  itg2addnc  38009  ftc1anclem5  38032  ftc2nc  38037  cnpwstotbnd  38132  lfl0f  39529  eqlkr2  39560  lcd0vvalN  42073  frlm0vald  42998  selvvvval  43032  evlselv  43034  mzpsubst  43194  mzpcompact2lem  43197  mzpcong  43418  hbtlem2  43570  mncn0  43585  mpaaeu  43596  aaitgo  43608  rngunsnply  43615  cantnfresb  43770  hashnzfzclim  44767  ofsubid  44769  dvconstbi  44779  binomcxplemnotnn0  44801  n0p  45494  snelmap  45531  nthrucw  47332  cjnpoly  47349  sinnpoly  47351  fvconst0ci  49378  fvconstdomi  49379  islmd  50152  iscmd  50153  aacllem  50288