Theorem fvconst2 7138

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  Vcvv 3436  {csn 4576   × cxp 5614  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489

This theorem is referenced by:  ovconst2  7526  mapsncnv  8817  ofsubeq0  12119  ofsubge0  12121  ser0f  13959  hashinf  14239  iserge0  15565  iseraltlem1  15586  sum0  15625  sumz  15626  harmonic  15763  prodf1f  15796  fprodntriv  15846  prod1  15848  setcmon  17991  0mhm  18724  mulgfval  18979  mulgpropd  19026  dprdsubg  19936  pwspjmhmmgpd  20244  0lmhm  20972  frlmlmod  21684  frlmlss  21686  frlmbas  21690  frlmip  21713  islindf4  21773  mplsubglem  21934  psdmvr  22082  coe1tm  22185  evls1maprnss  22291  mdetuni0  22534  txkgen  23565  xkofvcn  23597  nmo0  24648  pcorevlem  24951  rrxip  25315  mbfpos  25577  0pval  25597  0pledm  25599  xrge0f  25657  itg2ge0  25661  ibl0  25713  bddibl  25766  dvcmul  25872  dvef  25909  rolle  25919  dveq0  25930  dv11cn  25931  ftc2  25976  tdeglem4  25990  ply1rem  26096  fta1g  26100  fta1blem  26101  0dgrb  26176  dgrnznn  26177  dgrlt  26197  plymul0or  26213  plydivlem4  26229  plyrem  26238  fta1  26241  vieta1lem2  26244  elqaalem3  26254  aaliou2  26273  ulmdvlem1  26334  dchrelbas2  27173  dchrisumlem3  27427  noetasuplem4  27673  noetainflem4  27677  axlowdimlem9  28926  axlowdimlem12  28929  axlowdimlem17  28934  0oval  30763  occllem  31278  ho01i  31803  0cnfn  31955  0lnfn  31960  nmfn0  31962  nlelchi  32036  opsqrlem2  32116  opsqrlem4  32118  opsqrlem5  32119  hmopidmchi  32126  elrspunidl  33388  coe1zfv  33546  mplvrpmmhm  33571  lbsdiflsp0  33634  breprexpnat  34642  circlemethnat  34649  circlevma  34650  connpconn  35267  txsconnlem  35272  cvxsconn  35275  cvmliftphtlem  35349  fullfunfv  35980  matunitlindflem1  37655  matunitlindflem2  37656  ptrecube  37659  poimirlem1  37660  poimirlem2  37661  poimirlem3  37662  poimirlem4  37663  poimirlem5  37664  poimirlem6  37665  poimirlem7  37666  poimirlem10  37669  poimirlem11  37670  poimirlem12  37671  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem22  37681  poimirlem23  37682  poimirlem28  37687  poimirlem29  37688  poimirlem30  37689  poimirlem31  37690  poimirlem32  37691  poimir  37692  broucube  37693  mblfinlem2  37697  itg2addnclem  37710  itg2addnc  37713  ftc1anclem5  37736  ftc2nc  37741  cnpwstotbnd  37836  lfl0f  39107  eqlkr2  39138  lcd0vvalN  41651  frlm0vald  42571  evlsvvval  42595  selvvvval  42617  evlselv  42619  mzpsubst  42780  mzpcompact2lem  42783  mzpcong  43004  hbtlem2  43156  mncn0  43171  mpaaeu  43182  aaitgo  43194  rngunsnply  43201  cantnfresb  43356  hashnzfzclim  44354  ofsubid  44356  dvconstbi  44366  binomcxplemnotnn0  44388  n0p  45081  snelmap  45118  cjnpoly  46919  sinnpoly  46921  fvconst0ci  48921  fvconstdomi  48922  islmd  49696  iscmd  49697  aacllem  49832