Theorem fvconst2 7223

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  Vcvv 3477  {csn 4630   × cxp 5686  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570

This theorem is referenced by:  ovconst2  7612  mapsncnv  8931  ofsubeq0  12260  ofsubge0  12262  ser0f  14092  hashinf  14370  iserge0  15693  iseraltlem1  15714  sum0  15753  sumz  15754  harmonic  15891  prodf1f  15924  fprodntriv  15974  prod1  15976  setcmon  18140  0mhm  18844  mulgfval  19099  mulgpropd  19146  dprdsubg  20058  pwspjmhmmgpd  20341  0lmhm  21056  frlmlmod  21786  frlmlss  21788  frlmbas  21792  frlmip  21815  islindf4  21875  mplsubglem  22036  coe1tm  22291  evls1maprnss  22397  mdetuni0  22642  txkgen  23675  xkofvcn  23707  nmo0  24771  pcorevlem  25072  rrxip  25437  mbfpos  25699  0pval  25719  0pledm  25721  xrge0f  25780  itg2ge0  25784  ibl0  25836  bddibl  25889  dvcmul  25995  dvef  26032  rolle  26042  dveq0  26053  dv11cn  26054  ftc2  26099  tdeglem4  26113  ply1rem  26219  fta1g  26223  fta1blem  26224  0dgrb  26299  dgrnznn  26300  dgrlt  26320  plymul0or  26336  plydivlem4  26352  plyrem  26361  fta1  26364  vieta1lem2  26367  elqaalem3  26377  aaliou2  26396  ulmdvlem1  26457  dchrelbas2  27295  dchrisumlem3  27549  noetasuplem4  27795  noetainflem4  27799  axlowdimlem9  28979  axlowdimlem12  28982  axlowdimlem17  28987  0oval  30816  occllem  31331  ho01i  31856  0cnfn  32008  0lnfn  32013  nmfn0  32015  nlelchi  32089  opsqrlem2  32169  opsqrlem4  32171  opsqrlem5  32172  hmopidmchi  32179  elrspunidl  33435  coe1zfv  33591  lbsdiflsp0  33653  breprexpnat  34627  circlemethnat  34634  circlevma  34635  connpconn  35219  txsconnlem  35224  cvxsconn  35227  cvmliftphtlem  35301  fullfunfv  35928  matunitlindflem1  37602  matunitlindflem2  37603  ptrecube  37606  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem28  37634  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  poimir  37639  broucube  37640  mblfinlem2  37644  itg2addnclem  37657  itg2addnc  37660  ftc1anclem5  37683  ftc2nc  37688  cnpwstotbnd  37783  lfl0f  39050  eqlkr2  39081  lcd0vvalN  41595  frlm0vald  42525  evlsvvval  42549  selvvvval  42571  evlselv  42573  mzpsubst  42735  mzpcompact2lem  42738  mzpcong  42960  hbtlem2  43112  mncn0  43127  mpaaeu  43138  aaitgo  43150  rngunsnply  43157  cantnfresb  43313  hashnzfzclim  44317  ofsubid  44319  dvconstbi  44329  binomcxplemnotnn0  44351  n0p  44982  snelmap  45021  fvconst0ci  48688  fvconstdomi  48689  aacllem  49031