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

Theorem fvconst2g 6963
Description: The value of a constant function. (Contributed by NM, 20-Aug-2005.)
Assertion
Ref Expression
fvconst2g ((𝐵𝐷𝐶𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Proof of Theorem fvconst2g
StepHypRef Expression
1 fconstg 6562 . 2 (𝐵𝐷 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2 fvconst 6921 . 2 (((𝐴 × {𝐵}):𝐴⟶{𝐵} ∧ 𝐶𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
31, 2sylan 580 1 ((𝐵𝐷𝐶𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2107  {csn 4563   × cxp 5551  wf 6347  cfv 6351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pr 5325
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-opab 5125  df-mpt 5143  df-id 5458  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-fv 6359
This theorem is referenced by:  fconst2g  6964  fvconst2  6965  ofc1  7425  ofc2  7426  caofid0l  7430  caofid0r  7431  caofid1  7432  caofid2  7433  fnsuppres  7851  ser0  13415  ser1const  13419  exp1  13428  expp1  13429  climconst2  14898  climaddc1  14984  climmulc2  14986  climsubc1  14987  climsubc2  14988  climlec2  15008  fsumconst  15137  supcvg  15203  prodf1  15239  prod0  15289  fprodconst  15324  seq1st  15907  algr0  15908  algrf  15909  ramz  16353  pwsbas  16752  pwsplusgval  16755  pwsmulrval  16756  pwsle  16757  pwsvscafval  16759  pwspjmhm  17979  pwsco1mhm  17981  pwsinvg  18144  mulgnngsum  18165  mulg1  18167  mulgnnp1  18168  mulgnnsubcl  18172  mulgnn0z  18186  mulgnndir  18188  mulgnn0di  18868  gsumconst  18976  pwslmod  19664  psrlidm  20104  coe1tm  20360  coe1fzgsumd  20389  evl1scad  20416  frlmvscaval  20830  decpmatid  21296  pmatcollpwscmatlem1  21315  lmconst  21787  cnconst2  21809  xkoptsub  22180  xkopt  22181  xkopjcn  22182  tmdgsum  22621  tmdgsum2  22622  symgtgp  22627  cstucnd  22810  pcoptcl  23542  pcopt  23543  pcopt2  23544  dvidlem  24430  dvconst  24431  dvnff  24437  dvn0  24438  dvcmul  24458  dvcmulf  24459  fta1blem  24679  plyeq0lem  24717  coemulc  24762  dgreq0  24772  dgrmulc  24778  qaa  24829  dchrisumlema  25980  suppovss  30343  ofcc  31253  ofcof  31254  sseqf  31538  sseqp1  31541  lpadleft  31842  cvmlift3lem9  32460  ismrer1  34986  frlmvscadiccat  39012  dvsinax  42064  stoweidlem21  42174  stoweidlem47  42200  elaa2  42387  zlmodzxzscm  44239  2sphere0  44571
  Copyright terms: Public domain W3C validator