Theorem fvconst2 6943

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Vcvv 3441  {csn 4525   × cxp 5517  ‘cfv 6324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332

This theorem is referenced by:  ovconst2  7308  mapsncnv  8440  ofsubeq0  11622  ofsubge0  11624  ser0f  13419  hashinf  13691  iserge0  15009  iseraltlem1  15030  sum0  15070  sumz  15071  harmonic  15206  prodf1f  15240  fprodntriv  15288  prod1  15290  setcmon  17339  0mhm  17976  mulgfval  18218  mulgpropd  18261  dprdsubg  19139  0lmhm  19805  frlmlmod  20438  frlmlss  20440  frlmbas  20444  frlmip  20467  islindf4  20527  mplsubglem  20672  coe1tm  20902  mdetuni0  21226  txkgen  22257  xkofvcn  22289  nmo0  23341  pcorevlem  23631  rrxip  23994  mbfpos  24255  0pval  24275  0pledm  24277  xrge0f  24335  itg2ge0  24339  ibl0  24390  bddibl  24443  dvcmul  24547  dvef  24583  rolle  24593  dveq0  24603  dv11cn  24604  ftc2  24647  tdeglem4  24661  ply1rem  24764  fta1g  24768  fta1blem  24769  0dgrb  24843  dgrnznn  24844  dgrlt  24863  plymul0or  24877  plydivlem4  24892  plyrem  24901  fta1  24904  vieta1lem2  24907  elqaalem3  24917  aaliou2  24936  ulmdvlem1  24995  dchrelbas2  25821  dchrisumlem3  26075  axlowdimlem9  26744  axlowdimlem12  26747  axlowdimlem17  26752  0oval  28571  occllem  29086  ho01i  29611  0cnfn  29763  0lnfn  29768  nmfn0  29770  nlelchi  29844  opsqrlem2  29924  opsqrlem4  29926  opsqrlem5  29927  hmopidmchi  29934  elrspunidl  31014  lbsdiflsp0  31110  breprexpnat  32015  circlemethnat  32022  circlevma  32023  connpconn  32595  txsconnlem  32600  cvxsconn  32603  cvmliftphtlem  32677  noetalem3  33332  fullfunfv  33521  matunitlindflem1  35053  matunitlindflem2  35054  ptrecube  35057  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem22  35079  poimirlem23  35080  poimirlem28  35085  poimirlem29  35086  poimirlem30  35087  poimirlem31  35088  poimirlem32  35089  poimir  35090  broucube  35091  mblfinlem2  35095  itg2addnclem  35108  itg2addnc  35111  ftc1anclem5  35134  ftc2nc  35139  cnpwstotbnd  35235  lfl0f  36365  eqlkr2  36396  lcd0vvalN  38909  uvcn0  39455  mzpsubst  39689  mzpcompact2lem  39692  mzpcong  39913  hbtlem2  40068  mncn0  40083  mpaaeu  40094  aaitgo  40106  rngunsnply  40117  hashnzfzclim  41026  ofsubid  41028  dvconstbi  41038  binomcxplemnotnn0  41060  n0p  41677  snelmap  41718  aacllem  45329