Theorem fvconst2 7201

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3464  {csn 4606   × cxp 5657  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544

This theorem is referenced by:  ovconst2  7592  mapsncnv  8912  ofsubeq0  12242  ofsubge0  12244  ser0f  14078  hashinf  14358  iserge0  15682  iseraltlem1  15703  sum0  15742  sumz  15743  harmonic  15880  prodf1f  15913  fprodntriv  15963  prod1  15965  setcmon  18105  0mhm  18802  mulgfval  19057  mulgpropd  19104  dprdsubg  20012  pwspjmhmmgpd  20293  0lmhm  21003  frlmlmod  21714  frlmlss  21716  frlmbas  21720  frlmip  21743  islindf4  21803  mplsubglem  21964  psdmvr  22112  coe1tm  22215  evls1maprnss  22321  mdetuni0  22564  txkgen  23595  xkofvcn  23627  nmo0  24679  pcorevlem  24982  rrxip  25347  mbfpos  25609  0pval  25629  0pledm  25631  xrge0f  25689  itg2ge0  25693  ibl0  25745  bddibl  25798  dvcmul  25904  dvef  25941  rolle  25951  dveq0  25962  dv11cn  25963  ftc2  26008  tdeglem4  26022  ply1rem  26128  fta1g  26132  fta1blem  26133  0dgrb  26208  dgrnznn  26209  dgrlt  26229  plymul0or  26245  plydivlem4  26261  plyrem  26270  fta1  26273  vieta1lem2  26276  elqaalem3  26286  aaliou2  26305  ulmdvlem1  26366  dchrelbas2  27205  dchrisumlem3  27459  noetasuplem4  27705  noetainflem4  27709  axlowdimlem9  28934  axlowdimlem12  28937  axlowdimlem17  28942  0oval  30774  occllem  31289  ho01i  31814  0cnfn  31966  0lnfn  31971  nmfn0  31973  nlelchi  32047  opsqrlem2  32127  opsqrlem4  32129  opsqrlem5  32130  hmopidmchi  32137  elrspunidl  33448  coe1zfv  33605  lbsdiflsp0  33671  breprexpnat  34671  circlemethnat  34678  circlevma  34679  connpconn  35262  txsconnlem  35267  cvxsconn  35270  cvmliftphtlem  35344  fullfunfv  35970  matunitlindflem1  37645  matunitlindflem2  37646  ptrecube  37649  poimirlem1  37650  poimirlem2  37651  poimirlem3  37652  poimirlem4  37653  poimirlem5  37654  poimirlem6  37655  poimirlem7  37656  poimirlem10  37659  poimirlem11  37660  poimirlem12  37661  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem22  37671  poimirlem23  37672  poimirlem28  37677  poimirlem29  37678  poimirlem30  37679  poimirlem31  37680  poimirlem32  37681  poimir  37682  broucube  37683  mblfinlem2  37687  itg2addnclem  37700  itg2addnc  37703  ftc1anclem5  37726  ftc2nc  37731  cnpwstotbnd  37826  lfl0f  39092  eqlkr2  39123  lcd0vvalN  41637  frlm0vald  42537  evlsvvval  42561  selvvvval  42583  evlselv  42585  mzpsubst  42746  mzpcompact2lem  42749  mzpcong  42971  hbtlem2  43123  mncn0  43138  mpaaeu  43149  aaitgo  43161  rngunsnply  43168  cantnfresb  43323  hashnzfzclim  44321  ofsubid  44323  dvconstbi  44333  binomcxplemnotnn0  44355  n0p  45049  snelmap  45086  fvconst0ci  48846  fvconstdomi  48847  islmd  49515  iscmd  49516  aacllem  49645