Theorem fvconst2 7061

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  Vcvv 3422  {csn 4558   × cxp 5578  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426

This theorem is referenced by:  ovconst2  7430  mapsncnv  8639  ofsubeq0  11900  ofsubge0  11902  ser0f  13704  hashinf  13977  iserge0  15300  iseraltlem1  15321  sum0  15361  sumz  15362  harmonic  15499  prodf1f  15532  fprodntriv  15580  prod1  15582  setcmon  17718  0mhm  18373  mulgfval  18617  mulgpropd  18660  dprdsubg  19542  0lmhm  20217  frlmlmod  20866  frlmlss  20868  frlmbas  20872  frlmip  20895  islindf4  20955  mplsubglem  21115  coe1tm  21354  mdetuni0  21678  txkgen  22711  xkofvcn  22743  nmo0  23805  pcorevlem  24095  rrxip  24459  mbfpos  24720  0pval  24740  0pledm  24742  xrge0f  24801  itg2ge0  24805  ibl0  24856  bddibl  24909  dvcmul  25013  dvef  25049  rolle  25059  dveq0  25069  dv11cn  25070  ftc2  25113  tdeglem4  25129  tdeglem4OLD  25130  ply1rem  25233  fta1g  25237  fta1blem  25238  0dgrb  25312  dgrnznn  25313  dgrlt  25332  plymul0or  25346  plydivlem4  25361  plyrem  25370  fta1  25373  vieta1lem2  25376  elqaalem3  25386  aaliou2  25405  ulmdvlem1  25464  dchrelbas2  26290  dchrisumlem3  26544  axlowdimlem9  27221  axlowdimlem12  27224  axlowdimlem17  27229  0oval  29051  occllem  29566  ho01i  30091  0cnfn  30243  0lnfn  30248  nmfn0  30250  nlelchi  30324  opsqrlem2  30404  opsqrlem4  30406  opsqrlem5  30407  hmopidmchi  30414  elrspunidl  31508  lbsdiflsp0  31609  breprexpnat  32514  circlemethnat  32521  circlevma  32522  connpconn  33097  txsconnlem  33102  cvxsconn  33105  cvmliftphtlem  33179  noetasuplem4  33866  noetainflem4  33870  fullfunfv  34176  matunitlindflem1  35700  matunitlindflem2  35701  ptrecube  35704  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem28  35732  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  poimir  35737  broucube  35738  mblfinlem2  35742  itg2addnclem  35755  itg2addnc  35758  ftc1anclem5  35781  ftc2nc  35786  cnpwstotbnd  35882  lfl0f  37010  eqlkr2  37041  lcd0vvalN  39554  frlm0vald  40187  pwspjmhmmgpd  40192  mhphf  40208  mzpsubst  40486  mzpcompact2lem  40489  mzpcong  40710  hbtlem2  40865  mncn0  40880  mpaaeu  40891  aaitgo  40903  rngunsnply  40914  hashnzfzclim  41829  ofsubid  41831  dvconstbi  41841  binomcxplemnotnn0  41863  n0p  42480  snelmap  42521  fvconst0ci  46074  fvconstdomi  46075  aacllem  46391