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 702	1 ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  Vcvv 3455  {csn 4590   × cxp 5661  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546

This theorem is referenced by:  ovconst2  7592  mapsncnv  8892  ofsubeq0  12216  ofsubge0  12218  ser0f  14093  hashinf  14373  iserge0  15714  iseraltlem1  15735  sum0  15774  sumz  15775  harmonic  15915  prodf1f  15948  fprodntriv  15998  prod1  16000  setcmon  18145  0mhm  18879  mulgfval  19136  mulgpropd  19183  dprdsubg  20097  pwspjmhmmgpd  20410  0lmhm  21142  frlmlmod  21880  frlmlss  21882  frlmbas  21886  frlmip  21909  islindf4  21969  mplsubglem  22129  evlsvvval  22225  selvvvval  22274  psdmvr  22313  coe1tm  22415  evls1maprnss  22519  mdetuni0  22759  txkgen  23790  xkofvcn  23822  nmo0  24873  pcorevlem  25166  rrxip  25530  mbfpos  25791  0pval  25811  0pledm  25813  xrge0f  25871  itg2ge0  25875  ibl0  25927  bddibl  25980  dvcmul  26084  dvef  26120  rolle  26130  dveq0  26140  dv11cn  26141  ftc2  26184  tdeglem4  26198  ply1rem  26304  fta1g  26308  fta1blem  26309  0dgrb  26384  dgrnznn  26385  dgrlt  26404  plymul0or  26420  plydivlem4  26438  plyrem  26447  fta1  26450  vieta1lem2  26453  elqaalem3  26463  aaliou2  26484  ulmdvlem1  26544  dchrelbas2  27382  dchrisumlem3  27636  noetasuplem4  27881  noetainflem4  27885  axlowdimlem9  29281  axlowdimlem12  29284  axlowdimlem17  29289  0oval  31121  occllem  31636  ho01i  32161  0cnfn  32313  0lnfn  32318  nmfn0  32320  nlelchi  32394  opsqrlem2  32474  opsqrlem4  32476  opsqrlem5  32477  hmopidmchi  32484  elrspunidl  33717  coe1zfv  33861  psrnzr  33883  selvascl  33888  selvply1rhm0  33897  mplvrpmmhm  33917  vieta  33951  lbsdiflsp0  33997  breprexpnat  35002  circlemethnat  35009  circlevma  35010  connpconn  35708  txsconnlem  35713  cvxsconn  35716  cvmliftphtlem  35790  fullfunfv  36420  matunitlindflem1  38248  matunitlindflem2  38249  ptrecube  38252  poimirlem1  38253  poimirlem2  38254  poimirlem3  38255  poimirlem4  38256  poimirlem5  38257  poimirlem6  38258  poimirlem7  38259  poimirlem10  38262  poimirlem11  38263  poimirlem12  38264  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  poimirlem22  38274  poimirlem23  38275  poimirlem28  38280  poimirlem29  38281  poimirlem30  38282  poimirlem31  38283  poimirlem32  38284  poimir  38285  broucube  38286  mblfinlem2  38290  itg2addnclem  38303  itg2addnc  38306  ftc1anclem5  38329  ftc2nc  38334  cnpwstotbnd  38429  lfl0f  39824  eqlkr2  39855  lcd0vvalN  42368  frlm0vald  43290  evlselv  43304  mzpsubst  43462  mzpcompact2lem  43465  mzpcong  43682  hbtlem2  43834  mncn0  43849  mpaaeu  43860  aaitgo  43872  rngunsnply  43879  cantnfresb  44034  hashnzfzclim  45015  ofsubid  45017  dvconstbi  45027  binomcxplemnotnn0  45049  n0p  45748  snelmap  45785  cjnpoly  47609  sinnpoly  47611  fvconst0ci  49652  fvconstdomi  49653  islmd  50426  iscmd  50427  aacllem  50584