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

Theorem fvconst2g 6105
Description: The value of a constant function. (Contributed by NM, 20-Aug-2005.)
Assertion
Ref Expression
fvconst2g  |-  ( ( B  e.  D  /\  C  e.  A )  ->  ( ( A  X.  { B } ) `  C )  =  B )

Proof of Theorem fvconst2g
StepHypRef Expression
1 fconstg 5763 . 2  |-  ( B  e.  D  ->  ( A  X.  { B }
) : A --> { B } )
2 fvconst 6070 . 2  |-  ( ( ( A  X.  { B } ) : A --> { B }  /\  C  e.  A )  ->  (
( A  X.  { B } ) `  C
)  =  B )
31, 2sylan 471 1  |-  ( ( B  e.  D  /\  C  e.  A )  ->  ( ( A  X.  { B } ) `  C )  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374    e. wcel 1762   {csn 4020    X. cxp 4990   -->wf 5575   ` cfv 5579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-fv 5587
This theorem is referenced by:  fconst2g  6106  fvconst2  6107  fnsuppresOLD  6112  ofc1  6538  ofc2  6539  caofid0l  6543  caofid0r  6544  caofid1  6545  caofid2  6546  fnsuppres  6917  ser0  12115  ser1const  12119  exp1  12128  expp1  12129  climconst2  13320  climaddc1  13406  climmulc2  13408  climsubc1  13409  climsubc2  13410  climlec2  13430  fsumconst  13554  supcvg  13619  seq1st  14048  algr0  14049  algrf  14050  ramz  14391  pwsbas  14731  pwsplusgval  14734  pwsmulrval  14735  pwsle  14736  pwsvscafval  14738  pwspjmhm  15802  pwsco1mhm  15804  mulg1  15942  mulgnnp1  15943  mulgnnsubcl  15947  mulgnn0z  15955  mulgnndir  15957  pwsinvg  15975  mulgnn0di  16623  gsumconst  16738  pwslmod  17392  psrlidm  17820  psrlidmOLD  17821  psrridmOLD  17823  coe1tm  18078  coe1fzgsumd  18108  evl1scad  18135  frlmvscaval  18560  frlmip  18569  decpmatid  19031  pmatcollpwscmatlem1  19050  lmconst  19521  cnconst2  19543  xkoptsub  19883  xkopt  19884  xkopjcn  19885  tmdgsum  20322  tmdgsum2  20323  symgtgp  20328  cstucnd  20515  pcoptcl  21249  pcopt  21250  pcopt2  21251  rrxip  21550  dvidlem  22047  dvconst  22048  dvnff  22054  dvn0  22055  dvcmul  22075  dvcmulf  22076  fta1blem  22297  plyeq0lem  22335  coemulc  22379  dgreq0  22389  dgrmulc  22395  qaa  22446  dchrisumlema  23394  gx1  24926  gxnn0suc  24928  ofcc  27731  ofcof  27732  sseqf  27957  sseqp1  27960  cvmlift3lem9  28398  prodf1  28588  prod0  28638  fprodconst  28671  ismrer1  29924  dvsinax  31196  stoweidlem21  31276  stoweidlem47  31302  zlmodzxzscm  31885
  Copyright terms: Public domain W3C validator