Theorem fvconst2 7224

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3480  {csn 4626   × cxp 5683  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569

This theorem is referenced by:  ovconst2  7613  mapsncnv  8933  ofsubeq0  12263  ofsubge0  12265  ser0f  14096  hashinf  14374  iserge0  15697  iseraltlem1  15718  sum0  15757  sumz  15758  harmonic  15895  prodf1f  15928  fprodntriv  15978  prod1  15980  setcmon  18132  0mhm  18832  mulgfval  19087  mulgpropd  19134  dprdsubg  20044  pwspjmhmmgpd  20325  0lmhm  21039  frlmlmod  21769  frlmlss  21771  frlmbas  21775  frlmip  21798  islindf4  21858  mplsubglem  22019  psdmvr  22173  coe1tm  22276  evls1maprnss  22382  mdetuni0  22627  txkgen  23660  xkofvcn  23692  nmo0  24756  pcorevlem  25059  rrxip  25424  mbfpos  25686  0pval  25706  0pledm  25708  xrge0f  25766  itg2ge0  25770  ibl0  25822  bddibl  25875  dvcmul  25981  dvef  26018  rolle  26028  dveq0  26039  dv11cn  26040  ftc2  26085  tdeglem4  26099  ply1rem  26205  fta1g  26209  fta1blem  26210  0dgrb  26285  dgrnznn  26286  dgrlt  26306  plymul0or  26322  plydivlem4  26338  plyrem  26347  fta1  26350  vieta1lem2  26353  elqaalem3  26363  aaliou2  26382  ulmdvlem1  26443  dchrelbas2  27281  dchrisumlem3  27535  noetasuplem4  27781  noetainflem4  27785  axlowdimlem9  28965  axlowdimlem12  28968  axlowdimlem17  28973  0oval  30807  occllem  31322  ho01i  31847  0cnfn  31999  0lnfn  32004  nmfn0  32006  nlelchi  32080  opsqrlem2  32160  opsqrlem4  32162  opsqrlem5  32163  hmopidmchi  32170  elrspunidl  33456  coe1zfv  33612  lbsdiflsp0  33677  breprexpnat  34649  circlemethnat  34656  circlevma  34657  connpconn  35240  txsconnlem  35245  cvxsconn  35248  cvmliftphtlem  35322  fullfunfv  35948  matunitlindflem1  37623  matunitlindflem2  37624  ptrecube  37627  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem28  37655  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  poimir  37660  broucube  37661  mblfinlem2  37665  itg2addnclem  37678  itg2addnc  37681  ftc1anclem5  37704  ftc2nc  37709  cnpwstotbnd  37804  lfl0f  39070  eqlkr2  39101  lcd0vvalN  41615  frlm0vald  42549  evlsvvval  42573  selvvvval  42595  evlselv  42597  mzpsubst  42759  mzpcompact2lem  42762  mzpcong  42984  hbtlem2  43136  mncn0  43151  mpaaeu  43162  aaitgo  43174  rngunsnply  43181  cantnfresb  43337  hashnzfzclim  44341  ofsubid  44343  dvconstbi  44353  binomcxplemnotnn0  44375  n0p  45050  snelmap  45087  fvconst0ci  48790  fvconstdomi  48791  aacllem  49320