Theorem fvconst2 6743

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

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2107  Vcvv 3398  {csn 4398   × cxp 5355  ‘cfv 6137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pr 5140

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-fv 6145

This theorem is referenced by:  ovconst2  7093  mapsncnv  8192  ofsubeq0  11375  ofsubge0  11377  ser0f  13176  hashinf  13444  iserge0  14803  iseraltlem1  14824  sum0  14863  sumz  14864  harmonic  14999  prodf1f  15031  fprodntriv  15079  prod1  15081  setcmon  17126  0mhm  17748  mulgpropd  17972  dprdsubg  18814  0lmhm  19439  mplsubglem  19835  coe1tm  20043  frlmlmod  20496  frlmlss  20498  frlmbas  20502  frlmip  20525  islindf4  20585  mdetuni0  20836  txkgen  21868  xkofvcn  21900  nmo0  22951  pcorevlem  23237  rrxip  23600  mbfpos  23859  0pval  23879  0pledm  23881  xrge0f  23939  itg2ge0  23943  ibl0  23994  bddibl  24047  dvcmul  24148  dvef  24184  rolle  24194  dveq0  24204  dv11cn  24205  ftc2  24248  tdeglem4  24261  ply1rem  24364  fta1g  24368  fta1blem  24369  0dgrb  24443  dgrnznn  24444  dgrlt  24463  plymul0or  24477  plydivlem4  24492  plyrem  24501  fta1  24504  vieta1lem2  24507  elqaalem3  24517  aaliou2  24536  ulmdvlem1  24595  dchrelbas2  25418  dchrisumlem3  25636  axlowdimlem9  26303  axlowdimlem12  26306  axlowdimlem17  26311  0oval  28219  occllem  28738  ho01i  29263  0cnfn  29415  0lnfn  29420  nmfn0  29422  nlelchi  29496  opsqrlem2  29576  opsqrlem4  29578  opsqrlem5  29579  hmopidmchi  29586  lbsdiflsp0  30444  breprexpnat  31318  circlemethnat  31325  circlevma  31326  connpconn  31820  txsconnlem  31825  cvxsconn  31828  cvmliftphtlem  31902  noetalem3  32458  fullfunfv  32647  matunitlindflem1  34036  matunitlindflem2  34037  ptrecube  34040  poimirlem1  34041  poimirlem2  34042  poimirlem3  34043  poimirlem4  34044  poimirlem5  34045  poimirlem6  34046  poimirlem7  34047  poimirlem10  34050  poimirlem11  34051  poimirlem12  34052  poimirlem16  34056  poimirlem17  34057  poimirlem19  34059  poimirlem20  34060  poimirlem22  34062  poimirlem23  34063  poimirlem28  34068  poimirlem29  34069  poimirlem30  34070  poimirlem31  34071  poimirlem32  34072  poimir  34073  broucube  34074  mblfinlem2  34078  itg2addnclem  34091  itg2addnc  34094  ftc1anclem5  34119  ftc2nc  34124  cnpwstotbnd  34225  lfl0f  35228  eqlkr2  35259  lcd0vvalN  37772  mzpsubst  38281  mzpcompact2lem  38284  mzpcong  38508  hbtlem2  38663  mncn0  38678  mpaaeu  38689  aaitgo  38701  rngunsnply  38712  hashnzfzclim  39487  ofsubid  39489  dvconstbi  39499  binomcxplemnotnn0  39521  n0p  40151  snelmap  40195  aacllem  43663