Theorem fvconst2 7236

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  Vcvv 3454  {csn 4588   × cxp 5654  ‘cfv 6561

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569

This theorem is used by:  ovconst2  7628  mapsncnv  8952  ofsubeq0  12347  ofsubge0  12349  ser0f  14228  hashinf  14509  iserge0  15860  iseraltlem1  15881  sum0  15919  sumz  15920  harmonic  16060  prodf1f  16093  fprodntriv  16141  prod1  16143  setcmon  18294  0mhm  19047  mulgfval  19311  mulgpropd  19358  dprdsubg  20273  pwspjmhmmgpd  20590  0lmhm  21348  frlmlmod  22088  frlmlss  22090  frlmbas  22094  frlmip  22117  islindf4  22177  mplsubglem  22339  evlsvvval  22435  selvvvval  22484  psdmvr  22523  coe1tm  22625  evls1maprnss  22729  mdetuni0  22969  matunitlindflem1  23027  matunitlindflem2  23028  txkgen  24004  xkofvcn  24036  nmo0  25087  pcorevlem  25380  rrxip  25744  mbfpos  26005  0pval  26025  0pledm  26027  xrge0f  26085  itg2ge0  26089  ibl0  26140  bddibl  26193  dvcmul  26297  dvef  26333  rolle  26343  dveq0  26353  dv11cn  26354  ftc2  26397  tdeglem4  26411  ply1rem  26517  fta1g  26521  fta1blem  26522  0dgrb  26598  dgrnznn  26599  dgrlt  26618  plymul0or  26632  plydivlem4  26650  plyrem  26659  fta1  26662  rnplynfin  26663  vieta1lem2  26667  elqaalem3  26677  aaliou2  26700  ulmdvlem1  26760  dchrelbas2  27597  dchrisumlem3  27851  noetasuplem4  28126  noetainflem4  28130  axlowdimlem9  29561  axlowdimlem12  29564  axlowdimlem17  29569  0oval  31423  occllem  31938  ho01i  32463  0cnfn  32615  0lnfn  32620  nmfn0  32622  nlelchi  32696  opsqrlem2  32776  opsqrlem4  32778  opsqrlem5  32779  hmopidmchi  32786  elrspunidl  34062  coe1zfv  34205  psrnzr  34227  selvascl  34232  selvply1rhm0  34241  mplvrpmmhm  34261  vieta  34295  lbsdiflsp0  34341  breprexpnat  35346  circlemethnat  35353  circlevma  35354  connpconn  36180  txsconnlem  36185  cvxsconn  36188  cvmliftphtlem  36262  fullfunfv  36902  ptrecube  38743  poimirlem1  38744  poimirlem2  38745  poimirlem3  38746  poimirlem4  38747  poimirlem5  38748  poimirlem6  38749  poimirlem7  38750  poimirlem10  38753  poimirlem11  38754  poimirlem12  38755  poimirlem16  38759  poimirlem17  38760  poimirlem19  38762  poimirlem20  38763  poimirlem22  38765  poimirlem23  38766  poimirlem28  38771  poimirlem29  38772  poimirlem30  38773  poimirlem31  38774  poimirlem32  38775  poimir  38776  broucube  38777  mblfinlem2  38781  itg2addnclem  38794  itg2addnc  38797  ftc1anclem5  38820  ftc2nc  38825  cnpwstotbnd  38934  lfl0f  40329  eqlkr2  40360  lcd0vvalN  42873  frlm0vald  43807  evlselv  43821  mzpsubst  43963  mzpcompact2lem  43966  mzpcong  44183  hbtlem2  44329  mncn0  44344  mpaaeu  44355  aaitgo  44367  rngunsnply  44374  cantnfresb  44529  hashnzfzclim  45509  ofsubid  45511  dvconstbi  45521  binomcxplemnotnn0  45543  n0p  46278  snelmap  46314  cjnpoly  48154  sinnpoly  48156  fvconst0ci  50220  fvconstdomi  50221  par2diag  50995  islmd  51063  iscmd  51064  aacllem  51251  veroquadmodzerod  51296