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

Theorem fvconst2 6454
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 6452 . 2 ((𝐵 ∈ V ∧ 𝐶𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
31, 2mpan 705 1 (𝐶𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wcel 1988  Vcvv 3195  {csn 4168   × cxp 5102  cfv 5876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-fv 5884
This theorem is referenced by:  ovconst2  6799  mapsncnv  7889  ofsubeq0  11002  ofsubge0  11004  ser0f  12837  hashinf  13105  iserge0  14372  iseraltlem1  14393  sum0  14433  sumz  14434  harmonic  14572  prodf1f  14605  fprodntriv  14653  prod1  14655  setcmon  16718  0mhm  17339  mulgpropd  17565  dprdsubg  18404  0lmhm  19021  mplsubglem  19415  coe1tm  19624  frlmlmod  20074  frlmlss  20076  frlmbas  20080  frlmip  20098  islindf4  20158  mdetuni0  20408  txkgen  21436  xkofvcn  21468  nmo0  22520  pcorevlem  22807  rrxip  23159  mbfpos  23399  0pval  23419  0pledm  23421  xrge0f  23479  itg2ge0  23483  ibl0  23534  bddibl  23587  dvcmul  23688  dvef  23724  rolle  23734  dveq0  23744  dv11cn  23745  ftc2  23788  tdeglem4  23801  ply1rem  23904  fta1g  23908  fta1blem  23909  0dgrb  23983  dgrnznn  23984  dgrlt  24003  plymul0or  24017  plydivlem4  24032  plyrem  24041  fta1  24044  vieta1lem2  24047  elqaalem3  24057  aaliou2  24076  ulmdvlem1  24135  dchrelbas2  24943  dchrisumlem3  25161  axlowdimlem9  25811  axlowdimlem12  25814  axlowdimlem17  25819  0oval  27613  occllem  28132  ho01i  28657  0cnfn  28809  0lnfn  28814  nmfn0  28816  nlelchi  28890  opsqrlem2  28970  opsqrlem4  28972  opsqrlem5  28973  hmopidmchi  28980  breprexpnat  30686  circlemethnat  30693  circlevma  30694  connpconn  31191  txsconnlem  31196  cvxsconn  31199  cvmliftphtlem  31273  noetalem3  31839  fullfunfv  32029  matunitlindflem1  33376  matunitlindflem2  33377  ptrecube  33380  poimirlem1  33381  poimirlem2  33382  poimirlem3  33383  poimirlem4  33384  poimirlem5  33385  poimirlem6  33386  poimirlem7  33387  poimirlem10  33390  poimirlem11  33391  poimirlem12  33392  poimirlem16  33396  poimirlem17  33397  poimirlem19  33399  poimirlem20  33400  poimirlem22  33402  poimirlem23  33403  poimirlem28  33408  poimirlem29  33409  poimirlem30  33410  poimirlem31  33411  poimirlem32  33412  poimir  33413  broucube  33414  mblfinlem2  33418  itg2addnclem  33432  itg2addnc  33435  ftc1anclem5  33460  ftc2nc  33465  cnpwstotbnd  33567  lfl0f  34175  eqlkr2  34206  lcd0vvalN  36721  mzpsubst  37130  mzpcompact2lem  37133  mzpcong  37358  hbtlem2  37513  mncn0  37528  mpaaeu  37539  aaitgo  37551  rngunsnply  37562  hashnzfzclim  38341  ofsubid  38343  dvconstbi  38353  binomcxplemnotnn0  38375  n0p  39029  snelmap  39074  aacllem  42312
  Copyright terms: Public domain W3C validator