Theorem fvconst2 7160

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3442  {csn 4582   × cxp 5630  ‘cfv 6500

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508

This theorem is referenced by:  ovconst2  7548  mapsncnv  8843  ofsubeq0  12154  ofsubge0  12156  ser0f  13990  hashinf  14270  iserge0  15596  iseraltlem1  15617  sum0  15656  sumz  15657  harmonic  15794  prodf1f  15827  fprodntriv  15877  prod1  15879  setcmon  18023  0mhm  18756  mulgfval  19011  mulgpropd  19058  dprdsubg  19967  pwspjmhmmgpd  20275  0lmhm  21004  frlmlmod  21716  frlmlss  21718  frlmbas  21722  frlmip  21745  islindf4  21805  mplsubglem  21966  evlsvvval  22060  psdmvr  22124  coe1tm  22227  evls1maprnss  22334  mdetuni0  22577  txkgen  23608  xkofvcn  23640  nmo0  24691  pcorevlem  24994  rrxip  25358  mbfpos  25620  0pval  25640  0pledm  25642  xrge0f  25700  itg2ge0  25704  ibl0  25756  bddibl  25809  dvcmul  25915  dvef  25952  rolle  25962  dveq0  25973  dv11cn  25974  ftc2  26019  tdeglem4  26033  ply1rem  26139  fta1g  26143  fta1blem  26144  0dgrb  26219  dgrnznn  26220  dgrlt  26240  plymul0or  26256  plydivlem4  26272  plyrem  26281  fta1  26284  vieta1lem2  26287  elqaalem3  26297  aaliou2  26316  ulmdvlem1  26377  dchrelbas2  27216  dchrisumlem3  27470  noetasuplem4  27716  noetainflem4  27720  axlowdimlem9  29035  axlowdimlem12  29038  axlowdimlem17  29043  0oval  30875  occllem  31390  ho01i  31915  0cnfn  32067  0lnfn  32072  nmfn0  32074  nlelchi  32148  opsqrlem2  32228  opsqrlem4  32230  opsqrlem5  32231  hmopidmchi  32238  elrspunidl  33520  coe1zfv  33682  mplvrpmmhm  33722  vieta  33756  lbsdiflsp0  33803  breprexpnat  34811  circlemethnat  34818  circlevma  34819  connpconn  35448  txsconnlem  35453  cvxsconn  35456  cvmliftphtlem  35530  fullfunfv  36160  matunitlindflem1  37861  matunitlindflem2  37862  ptrecube  37865  poimirlem1  37866  poimirlem2  37867  poimirlem3  37868  poimirlem4  37869  poimirlem5  37870  poimirlem6  37871  poimirlem7  37872  poimirlem10  37875  poimirlem11  37876  poimirlem12  37877  poimirlem16  37881  poimirlem17  37882  poimirlem19  37884  poimirlem20  37885  poimirlem22  37887  poimirlem23  37888  poimirlem28  37893  poimirlem29  37894  poimirlem30  37895  poimirlem31  37896  poimirlem32  37897  poimir  37898  broucube  37899  mblfinlem2  37903  itg2addnclem  37916  itg2addnc  37919  ftc1anclem5  37942  ftc2nc  37947  cnpwstotbnd  38042  lfl0f  39439  eqlkr2  39470  lcd0vvalN  41983  frlm0vald  42903  selvvvval  42937  evlselv  42939  mzpsubst  43099  mzpcompact2lem  43102  mzpcong  43323  hbtlem2  43475  mncn0  43490  mpaaeu  43501  aaitgo  43513  rngunsnply  43520  cantnfresb  43675  hashnzfzclim  44672  ofsubid  44674  dvconstbi  44684  binomcxplemnotnn0  44706  n0p  45399  snelmap  45436  nthrucw  47238  cjnpoly  47243  sinnpoly  47245  fvconst0ci  49244  fvconstdomi  49245  islmd  50018  iscmd  50019  aacllem  50154