Theorem fvconst2 7184

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  Vcvv 3453  {csn 4581   × cxp 5643  ‘cfv 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-fv 6525

This theorem is referenced by:  ovconst2  7572  mapsncnv  8871  ofsubeq0  12189  ofsubge0  12191  ser0f  14065  hashinf  14345  iserge0  15671  iseraltlem1  15692  sum0  15731  sumz  15732  harmonic  15872  prodf1f  15905  fprodntriv  15955  prod1  15957  setcmon  18103  0mhm  18836  mulgfval  19094  mulgpropd  19141  dprdsubg  20049  pwspjmhmmgpd  20355  0lmhm  21087  frlmlmod  21781  frlmlss  21783  frlmbas  21787  frlmip  21810  islindf4  21870  mplsubglem  22030  evlsvvval  22126  selvvvval  22175  psdmvr  22214  coe1tm  22316  evls1maprnss  22421  mdetuni0  22661  txkgen  23692  xkofvcn  23724  nmo0  24775  pcorevlem  25068  rrxip  25432  mbfpos  25693  0pval  25713  0pledm  25715  xrge0f  25773  itg2ge0  25777  ibl0  25829  bddibl  25882  dvcmul  25986  dvef  26022  rolle  26032  dveq0  26042  dv11cn  26043  ftc2  26086  tdeglem4  26100  ply1rem  26206  fta1g  26210  fta1blem  26211  0dgrb  26286  dgrnznn  26287  dgrlt  26306  plymul0or  26322  plydivlem4  26337  plyrem  26346  fta1  26349  vieta1lem2  26352  elqaalem3  26362  aaliou2  26381  ulmdvlem1  26440  dchrelbas2  27278  dchrisumlem3  27532  noetasuplem4  27777  noetainflem4  27781  axlowdimlem9  29097  axlowdimlem12  29100  axlowdimlem17  29105  0oval  30937  occllem  31452  ho01i  31977  0cnfn  32129  0lnfn  32134  nmfn0  32136  nlelchi  32210  opsqrlem2  32290  opsqrlem4  32292  opsqrlem5  32293  hmopidmchi  32300  elrspunidl  33575  coe1zfv  33747  psrnzr  33770  selvascl  33775  selvply1rhm0  33784  mplvrpmmhm  33804  vieta  33838  lbsdiflsp0  33884  breprexpnat  34892  circlemethnat  34899  circlevma  34900  connpconn  35549  txsconnlem  35554  cvxsconn  35557  cvmliftphtlem  35631  fullfunfv  36261  matunitlindflem1  38079  matunitlindflem2  38080  ptrecube  38083  poimirlem1  38084  poimirlem2  38085  poimirlem3  38086  poimirlem4  38087  poimirlem5  38088  poimirlem6  38089  poimirlem7  38090  poimirlem10  38093  poimirlem11  38094  poimirlem12  38095  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  poimirlem22  38105  poimirlem23  38106  poimirlem28  38111  poimirlem29  38112  poimirlem30  38113  poimirlem31  38114  poimirlem32  38115  poimir  38116  broucube  38117  mblfinlem2  38121  itg2addnclem  38134  itg2addnc  38137  ftc1anclem5  38160  ftc2nc  38165  cnpwstotbnd  38260  lfl0f  39657  eqlkr2  39688  lcd0vvalN  42201  frlm0vald  43121  evlselv  43135  mzpsubst  43293  mzpcompact2lem  43296  mzpcong  43513  hbtlem2  43665  mncn0  43680  mpaaeu  43691  aaitgo  43703  rngunsnply  43710  cantnfresb  43865  hashnzfzclim  44862  ofsubid  44864  dvconstbi  44874  binomcxplemnotnn0  44896  n0p  45589  snelmap  45626  nthrucw  47426  cjnpoly  47447  sinnpoly  47449  fvconst0ci  49476  fvconstdomi  49477  islmd  50250  iscmd  50251  aacllem  50386