Theorem fvconst2 7159

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 7157	. 2 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
3	1, 2	mpan 691	1 ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3429  {csn 4567   × cxp 5629  ‘cfv 6498

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506

This theorem is referenced by:  ovconst2  7547  mapsncnv  8841  ofsubeq0  12156  ofsubge0  12158  ser0f  14017  hashinf  14297  iserge0  15623  iseraltlem1  15644  sum0  15683  sumz  15684  harmonic  15824  prodf1f  15857  fprodntriv  15907  prod1  15909  setcmon  18054  0mhm  18787  mulgfval  19045  mulgpropd  19092  dprdsubg  20001  pwspjmhmmgpd  20307  0lmhm  21035  frlmlmod  21729  frlmlss  21731  frlmbas  21735  frlmip  21758  islindf4  21818  mplsubglem  21977  evlsvvval  22071  psdmvr  22135  coe1tm  22238  evls1maprnss  22343  mdetuni0  22586  txkgen  23617  xkofvcn  23649  nmo0  24700  pcorevlem  24993  rrxip  25357  mbfpos  25618  0pval  25638  0pledm  25640  xrge0f  25698  itg2ge0  25702  ibl0  25754  bddibl  25807  dvcmul  25911  dvef  25947  rolle  25957  dveq0  25967  dv11cn  25968  ftc2  26011  tdeglem4  26025  ply1rem  26131  fta1g  26135  fta1blem  26136  0dgrb  26211  dgrnznn  26212  dgrlt  26231  plymul0or  26247  plydivlem4  26262  plyrem  26271  fta1  26274  vieta1lem2  26277  elqaalem3  26287  aaliou2  26306  ulmdvlem1  26365  dchrelbas2  27200  dchrisumlem3  27454  noetasuplem4  27700  noetainflem4  27704  axlowdimlem9  29019  axlowdimlem12  29022  axlowdimlem17  29027  0oval  30859  occllem  31374  ho01i  31899  0cnfn  32051  0lnfn  32056  nmfn0  32058  nlelchi  32132  opsqrlem2  32212  opsqrlem4  32214  opsqrlem5  32215  hmopidmchi  32222  elrspunidl  33488  coe1zfv  33650  mplvrpmmhm  33690  vieta  33724  lbsdiflsp0  33770  breprexpnat  34778  circlemethnat  34785  circlevma  34786  connpconn  35417  txsconnlem  35422  cvxsconn  35425  cvmliftphtlem  35499  fullfunfv  36129  matunitlindflem1  37937  matunitlindflem2  37938  ptrecube  37941  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  poimirlem28  37969  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  poimir  37974  broucube  37975  mblfinlem2  37979  itg2addnclem  37992  itg2addnc  37995  ftc1anclem5  38018  ftc2nc  38023  cnpwstotbnd  38118  lfl0f  39515  eqlkr2  39546  lcd0vvalN  42059  frlm0vald  42984  selvvvval  43018  evlselv  43020  mzpsubst  43180  mzpcompact2lem  43183  mzpcong  43400  hbtlem2  43552  mncn0  43567  mpaaeu  43578  aaitgo  43590  rngunsnply  43597  cantnfresb  43752  hashnzfzclim  44749  ofsubid  44751  dvconstbi  44761  binomcxplemnotnn0  44783  n0p  45476  snelmap  45513  nthrucw  47316  cjnpoly  47337  sinnpoly  47339  fvconst0ci  49366  fvconstdomi  49367  islmd  50140  iscmd  50141  aacllem  50276