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 4573   × cxp 5612  ‘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 5232  ax-nul 5242  ax-pr 5368

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 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  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  12122  ofsubge0  12124  ser0f  13962  hashinf  14242  iserge0  15568  iseraltlem1  15589  sum0  15628  sumz  15629  harmonic  15766  prodf1f  15799  fprodntriv  15849  prod1  15851  setcmon  17994  0mhm  18727  mulgfval  18982  mulgpropd  19029  dprdsubg  19938  pwspjmhmmgpd  20246  0lmhm  20974  frlmlmod  21686  frlmlss  21688  frlmbas  21692  frlmip  21715  islindf4  21775  mplsubglem  21936  psdmvr  22084  coe1tm  22187  evls1maprnss  22293  mdetuni0  22536  txkgen  23567  xkofvcn  23599  nmo0  24650  pcorevlem  24953  rrxip  25317  mbfpos  25579  0pval  25599  0pledm  25601  xrge0f  25659  itg2ge0  25663  ibl0  25715  bddibl  25768  dvcmul  25874  dvef  25911  rolle  25921  dveq0  25932  dv11cn  25933  ftc2  25978  tdeglem4  25992  ply1rem  26098  fta1g  26102  fta1blem  26103  0dgrb  26178  dgrnznn  26179  dgrlt  26199  plymul0or  26215  plydivlem4  26231  plyrem  26240  fta1  26243  vieta1lem2  26246  elqaalem3  26256  aaliou2  26275  ulmdvlem1  26336  dchrelbas2  27175  dchrisumlem3  27429  noetasuplem4  27675  noetainflem4  27679  axlowdimlem9  28928  axlowdimlem12  28931  axlowdimlem17  28936  0oval  30768  occllem  31283  ho01i  31808  0cnfn  31960  0lnfn  31965  nmfn0  31967  nlelchi  32041  opsqrlem2  32121  opsqrlem4  32123  opsqrlem5  32124  hmopidmchi  32131  elrspunidl  33393  coe1zfv  33551  mplvrpmmhm  33576  lbsdiflsp0  33639  breprexpnat  34647  circlemethnat  34654  circlevma  34655  connpconn  35279  txsconnlem  35284  cvxsconn  35287  cvmliftphtlem  35361  fullfunfv  35991  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  39167  eqlkr2  39198  lcd0vvalN  41711  frlm0vald  42631  evlsvvval  42655  selvvvval  42677  evlselv  42679  mzpsubst  42840  mzpcompact2lem  42843  mzpcong  43064  hbtlem2  43216  mncn0  43231  mpaaeu  43242  aaitgo  43254  rngunsnply  43261  cantnfresb  43416  hashnzfzclim  44414  ofsubid  44416  dvconstbi  44426  binomcxplemnotnn0  44448  n0p  45141  snelmap  45178  nthrucw  46983  cjnpoly  46988  sinnpoly  46990  fvconst0ci  48990  fvconstdomi  48991  islmd  49765  iscmd  49766  aacllem  49901