Theorem fvconst2 7202

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3451  {csn 4584   × cxp 5649  ‘cfv 6531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539

This theorem is used by:  ovconst2  7593  mapsncnv  8905  ofsubeq0  12298  ofsubge0  12300  ser0f  14178  hashinf  14459  iserge0  15808  iseraltlem1  15829  sum0  15867  sumz  15868  harmonic  16008  prodf1f  16041  fprodntriv  16089  prod1  16091  setcmon  18242  0mhm  18995  mulgfval  19259  mulgpropd  19306  dprdsubg  20220  pwspjmhmmgpd  20537  0lmhm  21295  frlmlmod  22035  frlmlss  22037  frlmbas  22041  frlmip  22064  islindf4  22124  mplsubglem  22286  evlsvvval  22382  selvvvval  22431  psdmvr  22470  coe1tm  22572  evls1maprnss  22676  mdetuni0  22916  matunitlindflem1  22974  matunitlindflem2  22975  txkgen  23951  xkofvcn  23983  nmo0  25034  pcorevlem  25327  rrxip  25691  mbfpos  25952  0pval  25972  0pledm  25974  xrge0f  26032  itg2ge0  26036  ibl0  26087  bddibl  26140  dvcmul  26244  dvef  26280  rolle  26290  dveq0  26300  dv11cn  26301  ftc2  26344  tdeglem4  26358  ply1rem  26464  fta1g  26468  fta1blem  26469  0dgrb  26545  dgrnznn  26546  dgrlt  26565  plymul0or  26581  plydivlem4  26599  plyrem  26608  fta1  26611  rnplynfin  26612  vieta1lem2  26616  elqaalem3  26626  aaliou2  26649  ulmdvlem1  26709  dchrelbas2  27546  dchrisumlem3  27800  noetasuplem4  28075  noetainflem4  28079  axlowdimlem9  29510  axlowdimlem12  29513  axlowdimlem17  29518  0oval  31372  occllem  31887  ho01i  32412  0cnfn  32564  0lnfn  32569  nmfn0  32571  nlelchi  32645  opsqrlem2  32725  opsqrlem4  32727  opsqrlem5  32728  hmopidmchi  32735  elrspunidl  33960  coe1zfv  34104  psrnzr  34126  selvascl  34131  selvply1rhm0  34140  mplvrpmmhm  34160  vieta  34194  lbsdiflsp0  34240  breprexpnat  35246  circlemethnat  35253  circlevma  35254  connpconn  35969  txsconnlem  35974  cvxsconn  35977  cvmliftphtlem  36051  fullfunfv  36681  ptrecube  38506  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem4  38510  poimirlem5  38511  poimirlem6  38512  poimirlem7  38513  poimirlem10  38516  poimirlem11  38517  poimirlem12  38518  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem22  38528  poimirlem23  38529  poimirlem28  38534  poimirlem29  38535  poimirlem30  38536  poimirlem31  38537  poimirlem32  38538  poimir  38539  broucube  38540  mblfinlem2  38544  itg2addnclem  38557  itg2addnc  38560  ftc1anclem5  38583  ftc2nc  38588  cnpwstotbnd  38699  lfl0f  40094  eqlkr2  40125  lcd0vvalN  42638  frlm0vald  43565  evlselv  43579  mzpsubst  43712  mzpcompact2lem  43715  mzpcong  43932  hbtlem2  44084  mncn0  44099  mpaaeu  44110  aaitgo  44122  rngunsnply  44129  cantnfresb  44284  hashnzfzclim  45265  ofsubid  45267  dvconstbi  45277  binomcxplemnotnn0  45299  n0p  46005  snelmap  46042  cjnpoly  47883  sinnpoly  47885  fvconst0ci  49943  fvconstdomi  49944  islmd  50717  iscmd  50718  aacllem  50883  veroquadmodzerod  50928