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

Theorem fvconst2g 6350
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 5990 . 2 (𝐵𝐷 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2 fvconst 6314 . 2 (((𝐴 × {𝐵}):𝐴⟶{𝐵} ∧ 𝐶𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
31, 2sylan 486 1 ((𝐵𝐷𝐶𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  {csn 4124   × cxp 5026  wf 5786  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-fv 5798
This theorem is referenced by:  fconst2g  6351  fvconst2  6352  ofc1  6796  ofc2  6797  caofid0l  6801  caofid0r  6802  caofid1  6803  caofid2  6804  fnsuppres  7187  ser0  12673  ser1const  12677  exp1  12686  expp1  12687  climconst2  14076  climaddc1  14162  climmulc2  14164  climsubc1  14165  climsubc2  14166  climlec2  14186  fsumconst  14313  supcvg  14376  prodf1  14411  prod0  14461  fprodconst  14496  seq1st  15071  algr0  15072  algrf  15073  ramz  15516  pwsbas  15919  pwsplusgval  15922  pwsmulrval  15923  pwsle  15924  pwsvscafval  15926  pwspjmhm  17140  pwsco1mhm  17142  pwsinvg  17300  mulg1  17320  mulgnnp1  17321  mulgnnsubcl  17325  mulgnn0z  17339  mulgnndir  17341  mulgnndirOLD  17342  mulgnn0di  18003  gsumconst  18106  pwslmod  18740  psrlidm  19173  coe1tm  19413  coe1fzgsumd  19442  evl1scad  19469  frlmvscaval  19877  decpmatid  20342  pmatcollpwscmatlem1  20361  lmconst  20823  cnconst2  20845  xkoptsub  21215  xkopt  21216  xkopjcn  21217  tmdgsum  21657  tmdgsum2  21658  symgtgp  21663  cstucnd  21846  pcoptcl  22577  pcopt  22578  pcopt2  22579  dvidlem  23430  dvconst  23431  dvnff  23437  dvn0  23438  dvcmul  23458  dvcmulf  23459  fta1blem  23677  plyeq0lem  23715  coemulc  23760  dgreq0  23770  dgrmulc  23776  qaa  23827  dchrisumlema  24922  ofcc  29329  ofcof  29330  sseqf  29615  sseqp1  29618  cvmlift3lem9  30397  ismrer1  32631  dvsinax  38625  stoweidlem21  38738  stoweidlem47  38764  elaa2  38951  zlmodzxzscm  41950
  Copyright terms: Public domain W3C validator