Theorem fvconst2 7204

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3474  {csn 4628   × cxp 5674  ‘cfv 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551

This theorem is referenced by:  ovconst2  7586  mapsncnv  8886  ofsubeq0  12208  ofsubge0  12210  ser0f  14020  hashinf  14294  iserge0  15606  iseraltlem1  15627  sum0  15666  sumz  15667  harmonic  15804  prodf1f  15837  fprodntriv  15885  prod1  15887  setcmon  18036  0mhm  18699  mulgfval  18951  mulgpropd  18995  dprdsubg  19893  pwspjmhmmgpd  20140  0lmhm  20650  frlmlmod  21303  frlmlss  21305  frlmbas  21309  frlmip  21332  islindf4  21392  mplsubglem  21557  coe1tm  21794  mdetuni0  22122  txkgen  23155  xkofvcn  23187  nmo0  24251  pcorevlem  24541  rrxip  24906  mbfpos  25167  0pval  25187  0pledm  25189  xrge0f  25248  itg2ge0  25252  ibl0  25303  bddibl  25356  dvcmul  25460  dvef  25496  rolle  25506  dveq0  25516  dv11cn  25517  ftc2  25560  tdeglem4  25576  tdeglem4OLD  25577  ply1rem  25680  fta1g  25684  fta1blem  25685  0dgrb  25759  dgrnznn  25760  dgrlt  25779  plymul0or  25793  plydivlem4  25808  plyrem  25817  fta1  25820  vieta1lem2  25823  elqaalem3  25833  aaliou2  25852  ulmdvlem1  25911  dchrelbas2  26737  dchrisumlem3  26991  noetasuplem4  27236  noetainflem4  27240  axlowdimlem9  28205  axlowdimlem12  28208  axlowdimlem17  28213  0oval  30036  occllem  30551  ho01i  31076  0cnfn  31228  0lnfn  31233  nmfn0  31235  nlelchi  31309  opsqrlem2  31389  opsqrlem4  31391  opsqrlem5  31392  hmopidmchi  31399  elrspunidl  32541  lbsdiflsp0  32706  evls1maprnss  32756  breprexpnat  33641  circlemethnat  33648  circlevma  33649  connpconn  34221  txsconnlem  34226  cvxsconn  34229  cvmliftphtlem  34303  fullfunfv  34914  matunitlindflem1  36479  matunitlindflem2  36480  ptrecube  36483  poimirlem1  36484  poimirlem2  36485  poimirlem3  36486  poimirlem4  36487  poimirlem5  36488  poimirlem6  36489  poimirlem7  36490  poimirlem10  36493  poimirlem11  36494  poimirlem12  36495  poimirlem16  36499  poimirlem17  36500  poimirlem19  36502  poimirlem20  36503  poimirlem22  36505  poimirlem23  36506  poimirlem28  36511  poimirlem29  36512  poimirlem30  36513  poimirlem31  36514  poimirlem32  36515  poimir  36516  broucube  36517  mblfinlem2  36521  itg2addnclem  36534  itg2addnc  36537  ftc1anclem5  36560  ftc2nc  36565  cnpwstotbnd  36660  lfl0f  37934  eqlkr2  37965  lcd0vvalN  40479  frlm0vald  41111  evlsvvval  41137  selvvvval  41159  evlselv  41161  mzpsubst  41476  mzpcompact2lem  41479  mzpcong  41701  hbtlem2  41856  mncn0  41871  mpaaeu  41882  aaitgo  41894  rngunsnply  41905  cantnfresb  42064  hashnzfzclim  43071  ofsubid  43073  dvconstbi  43083  binomcxplemnotnn0  43105  n0p  43720  snelmap  43761  fvconst0ci  47515  fvconstdomi  47516  aacllem  47838