Theorem fvconst2 7207

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3453  {csn 4587   × cxp 5657  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545

This theorem is used by:  ovconst2  7598  mapsncnv  8904  ofsubeq0  12243  ofsubge0  12245  ser0f  14123  hashinf  14403  iserge0  15752  iseraltlem1  15773  sum0  15811  sumz  15812  harmonic  15952  prodf1f  15985  fprodntriv  16035  prod1  16037  setcmon  18182  0mhm  18934  mulgfval  19198  mulgpropd  19245  dprdsubg  20159  pwspjmhmmgpd  20474  0lmhm  21230  frlmlmod  21968  frlmlss  21970  frlmbas  21974  frlmip  21997  islindf4  22057  mplsubglem  22219  evlsvvval  22315  selvvvval  22364  psdmvr  22403  coe1tm  22505  evls1maprnss  22609  mdetuni0  22849  matunitlindflem1  22907  matunitlindflem2  22908  txkgen  23884  xkofvcn  23916  nmo0  24967  pcorevlem  25260  rrxip  25624  mbfpos  25885  0pval  25905  0pledm  25907  xrge0f  25965  itg2ge0  25969  ibl0  26021  bddibl  26074  dvcmul  26178  dvef  26214  rolle  26224  dveq0  26234  dv11cn  26235  ftc2  26278  tdeglem4  26292  ply1rem  26398  fta1g  26402  fta1blem  26403  0dgrb  26479  dgrnznn  26480  dgrlt  26499  plymul0or  26515  plydivlem4  26533  plyrem  26542  fta1  26545  rnplynfin  26546  vieta1lem2  26550  elqaalem3  26560  aaliou2  26583  ulmdvlem1  26643  dchrelbas2  27481  dchrisumlem3  27735  noetasuplem4  27980  noetainflem4  27984  axlowdimlem9  29415  axlowdimlem12  29418  axlowdimlem17  29423  0oval  31277  occllem  31792  ho01i  32317  0cnfn  32469  0lnfn  32474  nmfn0  32476  nlelchi  32550  opsqrlem2  32630  opsqrlem4  32632  opsqrlem5  32633  hmopidmchi  32640  elrspunidl  33864  coe1zfv  34008  psrnzr  34030  selvascl  34035  selvply1rhm0  34044  mplvrpmmhm  34064  vieta  34098  lbsdiflsp0  34144  breprexpnat  35150  circlemethnat  35157  circlevma  35158  connpconn  35822  txsconnlem  35827  cvxsconn  35830  cvmliftphtlem  35904  fullfunfv  36534  ptrecube  38377  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem4  38381  poimirlem5  38382  poimirlem6  38383  poimirlem7  38384  poimirlem10  38387  poimirlem11  38388  poimirlem12  38389  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem22  38399  poimirlem23  38400  poimirlem28  38405  poimirlem29  38406  poimirlem30  38407  poimirlem31  38408  poimirlem32  38409  poimir  38410  broucube  38411  mblfinlem2  38415  itg2addnclem  38428  itg2addnc  38431  ftc1anclem5  38454  ftc2nc  38459  cnpwstotbnd  38555  lfl0f  39950  eqlkr2  39981  lcd0vvalN  42494  frlm0vald  43429  evlselv  43443  mzpsubst  43601  mzpcompact2lem  43604  mzpcong  43821  hbtlem2  43973  mncn0  43988  mpaaeu  43999  aaitgo  44011  rngunsnply  44018  cantnfresb  44173  hashnzfzclim  45154  ofsubid  45156  dvconstbi  45166  binomcxplemnotnn0  45188  n0p  45887  snelmap  45924  cjnpoly  47765  sinnpoly  47767  fvconst0ci  49825  fvconstdomi  49826  islmd  50599  iscmd  50600  aacllem  50780  veroquadmodzerod  50825