Theorem fvconst2 7144

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3437  {csn 4575   × cxp 5617  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494

This theorem is referenced by:  ovconst2  7532  mapsncnv  8823  ofsubeq0  12129  ofsubge0  12131  ser0f  13964  hashinf  14244  iserge0  15570  iseraltlem1  15591  sum0  15630  sumz  15631  harmonic  15768  prodf1f  15801  fprodntriv  15851  prod1  15853  setcmon  17996  0mhm  18729  mulgfval  18984  mulgpropd  19031  dprdsubg  19940  pwspjmhmmgpd  20248  0lmhm  20976  frlmlmod  21688  frlmlss  21690  frlmbas  21694  frlmip  21717  islindf4  21777  mplsubglem  21937  psdmvr  22085  coe1tm  22188  evls1maprnss  22294  mdetuni0  22537  txkgen  23568  xkofvcn  23600  nmo0  24651  pcorevlem  24954  rrxip  25318  mbfpos  25580  0pval  25600  0pledm  25602  xrge0f  25660  itg2ge0  25664  ibl0  25716  bddibl  25769  dvcmul  25875  dvef  25912  rolle  25922  dveq0  25933  dv11cn  25934  ftc2  25979  tdeglem4  25993  ply1rem  26099  fta1g  26103  fta1blem  26104  0dgrb  26179  dgrnznn  26180  dgrlt  26200  plymul0or  26216  plydivlem4  26232  plyrem  26241  fta1  26244  vieta1lem2  26247  elqaalem3  26257  aaliou2  26276  ulmdvlem1  26337  dchrelbas2  27176  dchrisumlem3  27430  noetasuplem4  27676  noetainflem4  27680  axlowdimlem9  28930  axlowdimlem12  28933  axlowdimlem17  28938  0oval  30770  occllem  31285  ho01i  31810  0cnfn  31962  0lnfn  31967  nmfn0  31969  nlelchi  32043  opsqrlem2  32123  opsqrlem4  32125  opsqrlem5  32126  hmopidmchi  32133  elrspunidl  33400  coe1zfv  33558  mplvrpmmhm  33594  lbsdiflsp0  33660  breprexpnat  34668  circlemethnat  34675  circlevma  34676  connpconn  35300  txsconnlem  35305  cvxsconn  35308  cvmliftphtlem  35382  fullfunfv  36012  matunitlindflem1  37676  matunitlindflem2  37677  ptrecube  37680  poimirlem1  37681  poimirlem2  37682  poimirlem3  37683  poimirlem4  37684  poimirlem5  37685  poimirlem6  37686  poimirlem7  37687  poimirlem10  37690  poimirlem11  37691  poimirlem12  37692  poimirlem16  37696  poimirlem17  37697  poimirlem19  37699  poimirlem20  37700  poimirlem22  37702  poimirlem23  37703  poimirlem28  37708  poimirlem29  37709  poimirlem30  37710  poimirlem31  37711  poimirlem32  37712  poimir  37713  broucube  37714  mblfinlem2  37718  itg2addnclem  37731  itg2addnc  37734  ftc1anclem5  37757  ftc2nc  37762  cnpwstotbnd  37857  lfl0f  39188  eqlkr2  39219  lcd0vvalN  41732  frlm0vald  42657  evlsvvval  42681  selvvvval  42703  evlselv  42705  mzpsubst  42865  mzpcompact2lem  42868  mzpcong  43089  hbtlem2  43241  mncn0  43256  mpaaeu  43267  aaitgo  43279  rngunsnply  43286  cantnfresb  43441  hashnzfzclim  44439  ofsubid  44441  dvconstbi  44451  binomcxplemnotnn0  44473  n0p  45166  snelmap  45203  nthrucw  47008  cjnpoly  47013  sinnpoly  47015  fvconst0ci  49015  fvconstdomi  49016  islmd  49790  iscmd  49791  aacllem  49926