Theorem fvconst2 7192

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  Vcvv 3457  {csn 4585   × cxp 5650  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fv 6533

This theorem is referenced by:  ovconst2  7580  mapsncnv  8879  ofsubeq0  12206  ofsubge0  12208  ser0f  14082  hashinf  14362  iserge0  15702  iseraltlem1  15723  sum0  15762  sumz  15763  harmonic  15903  prodf1f  15936  fprodntriv  15986  prod1  15988  setcmon  18134  0mhm  18868  mulgfval  19126  mulgpropd  19173  dprdsubg  20087  pwspjmhmmgpd  20400  0lmhm  21130  frlmlmod  21859  frlmlss  21861  frlmbas  21865  frlmip  21888  islindf4  21948  mplsubglem  22108  evlsvvval  22204  selvvvval  22253  psdmvr  22292  coe1tm  22394  evls1maprnss  22499  mdetuni0  22739  txkgen  23770  xkofvcn  23802  nmo0  24853  pcorevlem  25146  rrxip  25510  mbfpos  25771  0pval  25791  0pledm  25793  xrge0f  25851  itg2ge0  25855  ibl0  25907  bddibl  25960  dvcmul  26064  dvef  26100  rolle  26110  dveq0  26120  dv11cn  26121  ftc2  26164  tdeglem4  26178  ply1rem  26284  fta1g  26288  fta1blem  26289  0dgrb  26364  dgrnznn  26365  dgrlt  26384  plymul0or  26400  plydivlem4  26418  plyrem  26427  fta1  26430  vieta1lem2  26433  elqaalem3  26443  aaliou2  26462  ulmdvlem1  26521  dchrelbas2  27359  dchrisumlem3  27613  noetasuplem4  27858  noetainflem4  27862  axlowdimlem9  29209  axlowdimlem12  29212  axlowdimlem17  29217  0oval  31049  occllem  31564  ho01i  32089  0cnfn  32241  0lnfn  32246  nmfn0  32248  nlelchi  32322  opsqrlem2  32402  opsqrlem4  32404  opsqrlem5  32405  hmopidmchi  32412  elrspunidl  33652  coe1zfv  33797  psrnzr  33819  selvascl  33824  selvply1rhm0  33833  mplvrpmmhm  33853  vieta  33887  lbsdiflsp0  33933  breprexpnat  34938  circlemethnat  34945  circlevma  34946  connpconn  35598  txsconnlem  35603  cvxsconn  35606  cvmliftphtlem  35680  fullfunfv  36310  matunitlindflem1  38127  matunitlindflem2  38128  ptrecube  38131  poimirlem1  38132  poimirlem2  38133  poimirlem3  38134  poimirlem4  38135  poimirlem5  38136  poimirlem6  38137  poimirlem7  38138  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  poimirlem22  38153  poimirlem23  38154  poimirlem28  38159  poimirlem29  38160  poimirlem30  38161  poimirlem31  38162  poimirlem32  38163  poimir  38164  broucube  38165  mblfinlem2  38169  itg2addnclem  38182  itg2addnc  38185  ftc1anclem5  38208  ftc2nc  38213  cnpwstotbnd  38308  lfl0f  39705  eqlkr2  39736  lcd0vvalN  42249  frlm0vald  43169  evlselv  43183  mzpsubst  43341  mzpcompact2lem  43344  mzpcong  43561  hbtlem2  43713  mncn0  43728  mpaaeu  43739  aaitgo  43751  rngunsnply  43758  cantnfresb  43913  hashnzfzclim  44896  ofsubid  44898  dvconstbi  44908  binomcxplemnotnn0  44930  n0p  45623  snelmap  45660  nthrucw  47460  cjnpoly  47481  sinnpoly  47483  fvconst0ci  49520  fvconstdomi  49521  islmd  50294  iscmd  50295  aacllem  50430