MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvconst2 Structured version   Visualization version   GIF version

Theorem fvconst2 7154
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
StepHypRef Expression
1 fvconst2.1 . 2 𝐵 ∈ V
2 fvconst2g 7152 . 2 ((𝐵 ∈ V ∧ 𝐶𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
31, 2mpan 689 1 (𝐶𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  Vcvv 3446  {csn 4587   × cxp 5632  cfv 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-fv 6505
This theorem is referenced by:  ovconst2  7535  mapsncnv  8832  ofsubeq0  12151  ofsubge0  12153  ser0f  13962  hashinf  14236  iserge0  15546  iseraltlem1  15567  sum0  15607  sumz  15608  harmonic  15745  prodf1f  15778  fprodntriv  15826  prod1  15828  setcmon  17974  0mhm  18631  mulgfval  18875  mulgpropd  18919  dprdsubg  19804  pwspjmhmmgpd  20044  0lmhm  20504  frlmlmod  21158  frlmlss  21160  frlmbas  21164  frlmip  21187  islindf4  21247  mplsubglem  21408  coe1tm  21647  mdetuni0  21973  txkgen  23006  xkofvcn  23038  nmo0  24102  pcorevlem  24392  rrxip  24757  mbfpos  25018  0pval  25038  0pledm  25040  xrge0f  25099  itg2ge0  25103  ibl0  25154  bddibl  25207  dvcmul  25311  dvef  25347  rolle  25357  dveq0  25367  dv11cn  25368  ftc2  25411  tdeglem4  25427  tdeglem4OLD  25428  ply1rem  25531  fta1g  25535  fta1blem  25536  0dgrb  25610  dgrnznn  25611  dgrlt  25630  plymul0or  25644  plydivlem4  25659  plyrem  25668  fta1  25671  vieta1lem2  25674  elqaalem3  25684  aaliou2  25703  ulmdvlem1  25762  dchrelbas2  26588  dchrisumlem3  26842  noetasuplem4  27087  noetainflem4  27091  axlowdimlem9  27902  axlowdimlem12  27905  axlowdimlem17  27910  0oval  29733  occllem  30248  ho01i  30773  0cnfn  30925  0lnfn  30930  nmfn0  30932  nlelchi  31006  opsqrlem2  31086  opsqrlem4  31088  opsqrlem5  31089  hmopidmchi  31096  elrspunidl  32206  lbsdiflsp0  32324  breprexpnat  33250  circlemethnat  33257  circlevma  33258  connpconn  33832  txsconnlem  33837  cvxsconn  33840  cvmliftphtlem  33914  fullfunfv  34535  matunitlindflem1  36077  matunitlindflem2  36078  ptrecube  36081  poimirlem1  36082  poimirlem2  36083  poimirlem3  36084  poimirlem4  36085  poimirlem5  36086  poimirlem6  36087  poimirlem7  36088  poimirlem10  36091  poimirlem11  36092  poimirlem12  36093  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem22  36103  poimirlem23  36104  poimirlem28  36109  poimirlem29  36110  poimirlem30  36111  poimirlem31  36112  poimirlem32  36113  poimir  36114  broucube  36115  mblfinlem2  36119  itg2addnclem  36132  itg2addnc  36135  ftc1anclem5  36158  ftc2nc  36163  cnpwstotbnd  36259  lfl0f  37534  eqlkr2  37565  lcd0vvalN  40079  frlm0vald  40730  mhphf  40774  mzpsubst  41074  mzpcompact2lem  41077  mzpcong  41299  hbtlem2  41454  mncn0  41469  mpaaeu  41480  aaitgo  41492  rngunsnply  41503  cantnfresb  41661  hashnzfzclim  42609  ofsubid  42611  dvconstbi  42621  binomcxplemnotnn0  42643  n0p  43258  snelmap  43299  fvconst0ci  46932  fvconstdomi  46933  aacllem  47255
  Copyright terms: Public domain W3C validator