Theorem fvconst2 7200

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3475  {csn 4627   × cxp 5673  ‘cfv 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  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 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548

This theorem is referenced by:  ovconst2  7582  mapsncnv  8883  ofsubeq0  12205  ofsubge0  12207  ser0f  14017  hashinf  14291  iserge0  15603  iseraltlem1  15624  sum0  15663  sumz  15664  harmonic  15801  prodf1f  15834  fprodntriv  15882  prod1  15884  setcmon  18033  0mhm  18696  mulgfval  18946  mulgpropd  18990  dprdsubg  19886  pwspjmhmmgpd  20131  0lmhm  20639  frlmlmod  21288  frlmlss  21290  frlmbas  21294  frlmip  21317  islindf4  21377  mplsubglem  21540  coe1tm  21777  mdetuni0  22105  txkgen  23138  xkofvcn  23170  nmo0  24234  pcorevlem  24524  rrxip  24889  mbfpos  25150  0pval  25170  0pledm  25172  xrge0f  25231  itg2ge0  25235  ibl0  25286  bddibl  25339  dvcmul  25443  dvef  25479  rolle  25489  dveq0  25499  dv11cn  25500  ftc2  25543  tdeglem4  25559  tdeglem4OLD  25560  ply1rem  25663  fta1g  25667  fta1blem  25668  0dgrb  25742  dgrnznn  25743  dgrlt  25762  plymul0or  25776  plydivlem4  25791  plyrem  25800  fta1  25803  vieta1lem2  25806  elqaalem3  25816  aaliou2  25835  ulmdvlem1  25894  dchrelbas2  26720  dchrisumlem3  26974  noetasuplem4  27219  noetainflem4  27223  axlowdimlem9  28188  axlowdimlem12  28191  axlowdimlem17  28196  0oval  30019  occllem  30534  ho01i  31059  0cnfn  31211  0lnfn  31216  nmfn0  31218  nlelchi  31292  opsqrlem2  31372  opsqrlem4  31374  opsqrlem5  31375  hmopidmchi  31382  elrspunidl  32504  lbsdiflsp0  32656  evls1maprnss  32705  breprexpnat  33584  circlemethnat  33591  circlevma  33592  connpconn  34164  txsconnlem  34169  cvxsconn  34172  cvmliftphtlem  34246  fullfunfv  34857  matunitlindflem1  36422  matunitlindflem2  36423  ptrecube  36426  poimirlem1  36427  poimirlem2  36428  poimirlem3  36429  poimirlem4  36430  poimirlem5  36431  poimirlem6  36432  poimirlem7  36433  poimirlem10  36436  poimirlem11  36437  poimirlem12  36438  poimirlem16  36442  poimirlem17  36443  poimirlem19  36445  poimirlem20  36446  poimirlem22  36448  poimirlem23  36449  poimirlem28  36454  poimirlem29  36455  poimirlem30  36456  poimirlem31  36457  poimirlem32  36458  poimir  36459  broucube  36460  mblfinlem2  36464  itg2addnclem  36477  itg2addnc  36480  ftc1anclem5  36503  ftc2nc  36508  cnpwstotbnd  36603  lfl0f  37877  eqlkr2  37908  lcd0vvalN  40422  frlm0vald  41059  evlsvvval  41085  selvvvval  41107  evlselv  41109  mzpsubst  41419  mzpcompact2lem  41422  mzpcong  41644  hbtlem2  41799  mncn0  41814  mpaaeu  41825  aaitgo  41837  rngunsnply  41848  cantnfresb  42007  hashnzfzclim  43014  ofsubid  43016  dvconstbi  43026  binomcxplemnotnn0  43048  n0p  43663  snelmap  43704  fvconst0ci  47427  fvconstdomi  47428  aacllem  47750