Theorem fvconst2 7209

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  Vcvv 3458  {csn 4594   × cxp 5664  ‘cfv 6543

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551

This theorem is used by:  ovconst2  7603  mapsncnv  8900  ofsubeq0  12233  ofsubge0  12235  ser0f  14111  hashinf  14391  iserge0  15738  iseraltlem1  15759  sum0  15798  sumz  15799  harmonic  15939  prodf1f  15972  fprodntriv  16022  prod1  16024  setcmon  18169  0mhm  18909  mulgfval  19166  mulgpropd  19213  dprdsubg  20127  pwspjmhmmgpd  20442  0lmhm  21198  frlmlmod  21936  frlmlss  21938  frlmbas  21942  frlmip  21965  islindf4  22025  mplsubglem  22185  evlsvvval  22281  selvvvval  22330  psdmvr  22369  coe1tm  22471  evls1maprnss  22575  mdetuni0  22815  txkgen  23846  xkofvcn  23878  nmo0  24929  pcorevlem  25222  rrxip  25586  mbfpos  25847  0pval  25867  0pledm  25869  xrge0f  25927  itg2ge0  25931  ibl0  25983  bddibl  26036  dvcmul  26140  dvef  26176  rolle  26186  dveq0  26196  dv11cn  26197  ftc2  26240  tdeglem4  26254  ply1rem  26360  fta1g  26364  fta1blem  26365  0dgrb  26440  dgrnznn  26441  dgrlt  26460  plymul0or  26476  plydivlem4  26494  plyrem  26503  fta1  26506  vieta1lem2  26509  elqaalem3  26519  aaliou2  26540  ulmdvlem1  26600  dchrelbas2  27438  dchrisumlem3  27692  noetasuplem4  27937  noetainflem4  27941  axlowdimlem9  29337  axlowdimlem12  29340  axlowdimlem17  29345  0oval  31177  occllem  31692  ho01i  32217  0cnfn  32369  0lnfn  32374  nmfn0  32376  nlelchi  32450  opsqrlem2  32530  opsqrlem4  32532  opsqrlem5  32533  hmopidmchi  32540  elrspunidl  33767  coe1zfv  33911  psrnzr  33933  selvascl  33938  selvply1rhm0  33947  mplvrpmmhm  33967  vieta  34001  lbsdiflsp0  34047  breprexpnat  35053  circlemethnat  35060  circlevma  35061  connpconn  35748  txsconnlem  35753  cvxsconn  35756  cvmliftphtlem  35830  fullfunfv  36460  matunitlindflem1  38308  matunitlindflem2  38309  ptrecube  38312  poimirlem1  38313  poimirlem2  38314  poimirlem3  38315  poimirlem4  38316  poimirlem5  38317  poimirlem6  38318  poimirlem7  38319  poimirlem10  38322  poimirlem11  38323  poimirlem12  38324  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  poimirlem22  38334  poimirlem23  38335  poimirlem28  38340  poimirlem29  38341  poimirlem30  38342  poimirlem31  38343  poimirlem32  38344  poimir  38345  broucube  38346  mblfinlem2  38350  itg2addnclem  38363  itg2addnc  38366  ftc1anclem5  38389  ftc2nc  38394  cnpwstotbnd  38489  lfl0f  39884  eqlkr2  39915  lcd0vvalN  42428  frlm0vald  43348  evlselv  43362  mzpsubst  43520  mzpcompact2lem  43523  mzpcong  43740  hbtlem2  43892  mncn0  43907  mpaaeu  43918  aaitgo  43930  rngunsnply  43937  cantnfresb  44092  hashnzfzclim  45073  ofsubid  45075  dvconstbi  45085  binomcxplemnotnn0  45107  n0p  45806  snelmap  45843  cjnpoly  47667  sinnpoly  47669  fvconst0ci  49710  fvconstdomi  49711  islmd  50484  iscmd  50485  aacllem  50662