Theorem fvconst2 7150

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3440  {csn 4580   × cxp 5622  ‘cfv 6492

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  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  7538  mapsncnv  8831  ofsubeq0  12142  ofsubge0  12144  ser0f  13978  hashinf  14258  iserge0  15584  iseraltlem1  15605  sum0  15644  sumz  15645  harmonic  15782  prodf1f  15815  fprodntriv  15865  prod1  15867  setcmon  18011  0mhm  18744  mulgfval  18999  mulgpropd  19046  dprdsubg  19955  pwspjmhmmgpd  20263  0lmhm  20992  frlmlmod  21704  frlmlss  21706  frlmbas  21710  frlmip  21733  islindf4  21793  mplsubglem  21954  evlsvvval  22048  psdmvr  22112  coe1tm  22215  evls1maprnss  22322  mdetuni0  22565  txkgen  23596  xkofvcn  23628  nmo0  24679  pcorevlem  24982  rrxip  25346  mbfpos  25608  0pval  25628  0pledm  25630  xrge0f  25688  itg2ge0  25692  ibl0  25744  bddibl  25797  dvcmul  25903  dvef  25940  rolle  25950  dveq0  25961  dv11cn  25962  ftc2  26007  tdeglem4  26021  ply1rem  26127  fta1g  26131  fta1blem  26132  0dgrb  26207  dgrnznn  26208  dgrlt  26228  plymul0or  26244  plydivlem4  26260  plyrem  26269  fta1  26272  vieta1lem2  26275  elqaalem3  26285  aaliou2  26304  ulmdvlem1  26365  dchrelbas2  27204  dchrisumlem3  27458  noetasuplem4  27704  noetainflem4  27708  axlowdimlem9  29023  axlowdimlem12  29026  axlowdimlem17  29031  0oval  30863  occllem  31378  ho01i  31903  0cnfn  32055  0lnfn  32060  nmfn0  32062  nlelchi  32136  opsqrlem2  32216  opsqrlem4  32218  opsqrlem5  32219  hmopidmchi  32226  elrspunidl  33509  coe1zfv  33671  mplvrpmmhm  33711  vieta  33736  lbsdiflsp0  33783  breprexpnat  34791  circlemethnat  34798  circlevma  34799  connpconn  35429  txsconnlem  35434  cvxsconn  35437  cvmliftphtlem  35511  fullfunfv  36141  matunitlindflem1  37813  matunitlindflem2  37814  ptrecube  37817  poimirlem1  37818  poimirlem2  37819  poimirlem3  37820  poimirlem4  37821  poimirlem5  37822  poimirlem6  37823  poimirlem7  37824  poimirlem10  37827  poimirlem11  37828  poimirlem12  37829  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem22  37839  poimirlem23  37840  poimirlem28  37845  poimirlem29  37846  poimirlem30  37847  poimirlem31  37848  poimirlem32  37849  poimir  37850  broucube  37851  mblfinlem2  37855  itg2addnclem  37868  itg2addnc  37871  ftc1anclem5  37894  ftc2nc  37899  cnpwstotbnd  37994  lfl0f  39325  eqlkr2  39356  lcd0vvalN  41869  frlm0vald  42790  selvvvval  42824  evlselv  42826  mzpsubst  42986  mzpcompact2lem  42989  mzpcong  43210  hbtlem2  43362  mncn0  43377  mpaaeu  43388  aaitgo  43400  rngunsnply  43407  cantnfresb  43562  hashnzfzclim  44559  ofsubid  44561  dvconstbi  44571  binomcxplemnotnn0  44593  n0p  45286  snelmap  45323  nthrucw  47126  cjnpoly  47131  sinnpoly  47133  fvconst0ci  49132  fvconstdomi  49133  islmd  49906  iscmd  49907  aacllem  50042