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

Theorem fvconst2 6510
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 6508 . 2 ((𝐵 ∈ V ∧ 𝐶𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
31, 2mpan 706 1 (𝐶𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  Vcvv 3231  {csn 4210   × cxp 5141  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934
This theorem is referenced by:  ovconst2  6856  mapsncnv  7946  ofsubeq0  11055  ofsubge0  11057  ser0f  12894  hashinf  13162  iserge0  14435  iseraltlem1  14456  sum0  14496  sumz  14497  harmonic  14635  prodf1f  14668  fprodntriv  14716  prod1  14718  setcmon  16784  0mhm  17405  mulgpropd  17631  dprdsubg  18469  0lmhm  19088  mplsubglem  19482  coe1tm  19691  frlmlmod  20141  frlmlss  20143  frlmbas  20147  frlmip  20165  islindf4  20225  mdetuni0  20475  txkgen  21503  xkofvcn  21535  nmo0  22586  pcorevlem  22872  rrxip  23224  mbfpos  23463  0pval  23483  0pledm  23485  xrge0f  23543  itg2ge0  23547  ibl0  23598  bddibl  23651  dvcmul  23752  dvef  23788  rolle  23798  dveq0  23808  dv11cn  23809  ftc2  23852  tdeglem4  23865  ply1rem  23968  fta1g  23972  fta1blem  23973  0dgrb  24047  dgrnznn  24048  dgrlt  24067  plymul0or  24081  plydivlem4  24096  plyrem  24105  fta1  24108  vieta1lem2  24111  elqaalem3  24121  aaliou2  24140  ulmdvlem1  24199  dchrelbas2  25007  dchrisumlem3  25225  axlowdimlem9  25875  axlowdimlem12  25878  axlowdimlem17  25883  0oval  27771  occllem  28290  ho01i  28815  0cnfn  28967  0lnfn  28972  nmfn0  28974  nlelchi  29048  opsqrlem2  29128  opsqrlem4  29130  opsqrlem5  29131  hmopidmchi  29138  breprexpnat  30840  circlemethnat  30847  circlevma  30848  connpconn  31343  txsconnlem  31348  cvxsconn  31351  cvmliftphtlem  31425  noetalem3  31990  fullfunfv  32179  matunitlindflem1  33535  matunitlindflem2  33536  ptrecube  33539  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem22  33561  poimirlem23  33562  poimirlem28  33567  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  poimir  33572  broucube  33573  mblfinlem2  33577  itg2addnclem  33591  itg2addnc  33594  ftc1anclem5  33619  ftc2nc  33624  cnpwstotbnd  33726  lfl0f  34674  eqlkr2  34705  lcd0vvalN  37219  mzpsubst  37628  mzpcompact2lem  37631  mzpcong  37856  hbtlem2  38011  mncn0  38026  mpaaeu  38037  aaitgo  38049  rngunsnply  38060  hashnzfzclim  38838  ofsubid  38840  dvconstbi  38850  binomcxplemnotnn0  38872  n0p  39523  snelmap  39568  aacllem  42875
  Copyright terms: Public domain W3C validator