Theorem fvconst2 7206

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  Vcvv 3472  {csn 4627   × cxp 5673  ‘cfv 6542

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550

This theorem is referenced by:  ovconst2  7589  mapsncnv  8889  ofsubeq0  12213  ofsubge0  12215  ser0f  14025  hashinf  14299  iserge0  15611  iseraltlem1  15632  sum0  15671  sumz  15672  harmonic  15809  prodf1f  15842  fprodntriv  15890  prod1  15892  setcmon  18041  0mhm  18736  mulgfval  18988  mulgpropd  19032  dprdsubg  19935  pwspjmhmmgpd  20216  0lmhm  20795  frlmlmod  21523  frlmlss  21525  frlmbas  21529  frlmip  21552  islindf4  21612  mplsubglem  21777  coe1tm  22015  mdetuni0  22343  txkgen  23376  xkofvcn  23408  nmo0  24472  pcorevlem  24773  rrxip  25138  mbfpos  25400  0pval  25420  0pledm  25422  xrge0f  25481  itg2ge0  25485  ibl0  25536  bddibl  25589  dvcmul  25695  dvef  25732  rolle  25742  dveq0  25752  dv11cn  25753  ftc2  25796  tdeglem4  25812  tdeglem4OLD  25813  ply1rem  25916  fta1g  25920  fta1blem  25921  0dgrb  25995  dgrnznn  25996  dgrlt  26016  plymul0or  26030  plydivlem4  26045  plyrem  26054  fta1  26057  vieta1lem2  26060  elqaalem3  26070  aaliou2  26089  ulmdvlem1  26148  dchrelbas2  26976  dchrisumlem3  27230  noetasuplem4  27475  noetainflem4  27479  axlowdimlem9  28475  axlowdimlem12  28478  axlowdimlem17  28483  0oval  30308  occllem  30823  ho01i  31348  0cnfn  31500  0lnfn  31505  nmfn0  31507  nlelchi  31581  opsqrlem2  31661  opsqrlem4  31663  opsqrlem5  31664  hmopidmchi  31671  elrspunidl  32820  lbsdiflsp0  32999  evls1maprnss  33050  breprexpnat  33944  circlemethnat  33951  circlevma  33952  connpconn  34524  txsconnlem  34529  cvxsconn  34532  cvmliftphtlem  34606  fullfunfv  35223  matunitlindflem1  36787  matunitlindflem2  36788  ptrecube  36791  poimirlem1  36792  poimirlem2  36793  poimirlem3  36794  poimirlem4  36795  poimirlem5  36796  poimirlem6  36797  poimirlem7  36798  poimirlem10  36801  poimirlem11  36802  poimirlem12  36803  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem22  36813  poimirlem23  36814  poimirlem28  36819  poimirlem29  36820  poimirlem30  36821  poimirlem31  36822  poimirlem32  36823  poimir  36824  broucube  36825  mblfinlem2  36829  itg2addnclem  36842  itg2addnc  36845  ftc1anclem5  36868  ftc2nc  36873  cnpwstotbnd  36968  lfl0f  38242  eqlkr2  38273  lcd0vvalN  40787  frlm0vald  41411  evlsvvval  41437  selvvvval  41459  evlselv  41461  mzpsubst  41788  mzpcompact2lem  41791  mzpcong  42013  hbtlem2  42168  mncn0  42183  mpaaeu  42194  aaitgo  42206  rngunsnply  42217  cantnfresb  42376  hashnzfzclim  43383  ofsubid  43385  dvconstbi  43395  binomcxplemnotnn0  43417  n0p  44031  snelmap  44072  fvconst0ci  47612  fvconstdomi  47613  aacllem  47935