Theorem fvconst2 7155

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3432  {csn 4562   × cxp 5623  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500

This theorem is referenced by:  ovconst2  7543  mapsncnv  8838  ofsubeq0  12154  ofsubge0  12156  ser0f  14015  hashinf  14295  iserge0  15621  iseraltlem1  15642  sum0  15681  sumz  15682  harmonic  15822  prodf1f  15855  fprodntriv  15905  prod1  15907  setcmon  18052  0mhm  18785  mulgfval  19043  mulgpropd  19090  dprdsubg  19999  pwspjmhmmgpd  20305  0lmhm  21037  frlmlmod  21731  frlmlss  21733  frlmbas  21737  frlmip  21760  islindf4  21820  mplsubglem  21980  evlsvvval  22076  selvvvval  22125  psdmvr  22164  coe1tm  22266  evls1maprnss  22371  mdetuni0  22611  txkgen  23642  xkofvcn  23674  nmo0  24725  pcorevlem  25018  rrxip  25382  mbfpos  25643  0pval  25663  0pledm  25665  xrge0f  25723  itg2ge0  25727  ibl0  25779  bddibl  25832  dvcmul  25936  dvef  25972  rolle  25982  dveq0  25992  dv11cn  25993  ftc2  26036  tdeglem4  26050  ply1rem  26156  fta1g  26160  fta1blem  26161  0dgrb  26236  dgrnznn  26237  dgrlt  26256  plymul0or  26272  plydivlem4  26287  plyrem  26296  fta1  26299  vieta1lem2  26302  elqaalem3  26312  aaliou2  26331  ulmdvlem1  26390  dchrelbas2  27225  dchrisumlem3  27479  noetasuplem4  27725  noetainflem4  27729  axlowdimlem9  29044  axlowdimlem12  29047  axlowdimlem17  29052  0oval  30884  occllem  31399  ho01i  31924  0cnfn  32076  0lnfn  32081  nmfn0  32083  nlelchi  32157  opsqrlem2  32237  opsqrlem4  32239  opsqrlem5  32240  hmopidmchi  32247  elrspunidl  33518  coe1zfv  33680  psrnzr  33703  selvascl  33708  selvply1rhm0  33717  mplvrpmmhm  33737  vieta  33771  lbsdiflsp0  33817  breprexpnat  34825  circlemethnat  34832  circlevma  34833  connpconn  35470  txsconnlem  35475  cvxsconn  35478  cvmliftphtlem  35552  fullfunfv  36182  matunitlindflem1  37990  matunitlindflem2  37991  ptrecube  37994  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem4  37998  poimirlem5  37999  poimirlem6  38000  poimirlem7  38001  poimirlem10  38004  poimirlem11  38005  poimirlem12  38006  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem22  38016  poimirlem23  38017  poimirlem28  38022  poimirlem29  38023  poimirlem30  38024  poimirlem31  38025  poimirlem32  38026  poimir  38027  broucube  38028  mblfinlem2  38032  itg2addnclem  38045  itg2addnc  38048  ftc1anclem5  38071  ftc2nc  38076  cnpwstotbnd  38171  lfl0f  39568  eqlkr2  39599  lcd0vvalN  42112  frlm0vald  43032  evlselv  43046  mzpsubst  43204  mzpcompact2lem  43207  mzpcong  43424  hbtlem2  43576  mncn0  43591  mpaaeu  43602  aaitgo  43614  rngunsnply  43621  cantnfresb  43776  hashnzfzclim  44773  ofsubid  44775  dvconstbi  44785  binomcxplemnotnn0  44807  n0p  45500  snelmap  45537  nthrucw  47338  cjnpoly  47359  sinnpoly  47361  fvconst0ci  49388  fvconstdomi  49389  islmd  50162  iscmd  50163  aacllem  50298