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

Theorem fvconst2g 6633
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 6254 . 2 (𝐵𝐷 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2 fvconst 6596 . 2 (((𝐴 × {𝐵}):𝐴⟶{𝐵} ∧ 𝐶𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
31, 2sylan 489 1 ((𝐵𝐷𝐶𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wcel 2140  {csn 4322   × cxp 5265  wf 6046  cfv 6050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-sep 4934  ax-nul 4942  ax-pr 5056
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3343  df-sbc 3578  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-fv 6058
This theorem is referenced by:  fconst2g  6634  fvconst2  6635  ofc1  7087  ofc2  7088  caofid0l  7092  caofid0r  7093  caofid1  7094  caofid2  7095  fnsuppres  7493  ser0  13068  ser1const  13072  exp1  13081  expp1  13082  climconst2  14499  climaddc1  14585  climmulc2  14587  climsubc1  14588  climsubc2  14589  climlec2  14609  fsumconst  14742  supcvg  14808  prodf1  14843  prod0  14893  fprodconst  14928  seq1st  15507  algr0  15508  algrf  15509  ramz  15952  pwsbas  16370  pwsplusgval  16373  pwsmulrval  16374  pwsle  16375  pwsvscafval  16377  pwspjmhm  17590  pwsco1mhm  17592  pwsinvg  17750  mulg1  17770  mulgnnp1  17771  mulgnnsubcl  17775  mulgnn0z  17789  mulgnndir  17791  mulgnndirOLD  17792  mulgnn0di  18452  gsumconst  18555  pwslmod  19193  psrlidm  19626  coe1tm  19866  coe1fzgsumd  19895  evl1scad  19922  frlmvscaval  20333  decpmatid  20798  pmatcollpwscmatlem1  20817  lmconst  21288  cnconst2  21310  xkoptsub  21680  xkopt  21681  xkopjcn  21682  tmdgsum  22121  tmdgsum2  22122  symgtgp  22127  cstucnd  22310  pcoptcl  23042  pcopt  23043  pcopt2  23044  dvidlem  23899  dvconst  23900  dvnff  23906  dvn0  23907  dvcmul  23927  dvcmulf  23928  fta1blem  24148  plyeq0lem  24186  coemulc  24231  dgreq0  24241  dgrmulc  24247  qaa  24298  dchrisumlema  25398  ofcc  30499  ofcof  30500  sseqf  30785  sseqp1  30788  cvmlift3lem9  31638  ismrer1  33969  dvsinax  40649  stoweidlem21  40760  stoweidlem47  40786  elaa2  40973  zlmodzxzscm  42664
  Copyright terms: Public domain W3C validator