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

Theorem fvconst2g 5934
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 5600 . 2  |-  ( B  e.  D  ->  ( A  X.  { B }
) : A --> { B } )
2 fvconst 5900 . 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 1369    e. wcel 1756   {csn 3880    X. cxp 4841   -->wf 5417   ` cfv 5421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pr 4534
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-mpt 4355  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-fv 5429
This theorem is referenced by:  fconst2g  5935  fvconst2  5936  fnsuppresOLD  5941  ofc1  6346  ofc2  6347  caofid0l  6351  caofid0r  6352  caofid1  6353  caofid2  6354  fnsuppres  6719  ser0  11861  ser1const  11865  exp1  11874  expp1  11875  climconst2  13029  climaddc1  13115  climmulc2  13117  climsubc1  13118  climsubc2  13119  climlec2  13139  fsumconst  13260  supcvg  13321  seq1st  13749  algr0  13750  algrf  13751  ramz  14089  pwsbas  14428  pwsplusgval  14431  pwsmulrval  14432  pwsle  14433  pwsvscafval  14435  pwspjmhm  15499  pwsco1mhm  15501  mulg1  15637  mulgnnp1  15638  mulgnnsubcl  15642  mulgnn0z  15650  mulgnndir  15652  pwsinvg  15670  mulgnn0di  16316  gsumconst  16430  pwslmod  17054  psrlidm  17477  psrlidmOLD  17478  psrridmOLD  17480  coe1tm  17729  evl1scad  17772  frlmvscaval  18197  frlmip  18206  lmconst  18868  cnconst2  18890  xkoptsub  19230  xkopt  19231  xkopjcn  19232  tmdgsum  19669  tmdgsum2  19670  symgtgp  19675  cstucnd  19862  pcoptcl  20596  pcopt  20597  pcopt2  20598  rrxip  20897  dvidlem  21393  dvconst  21394  dvnff  21400  dvn0  21401  dvcmul  21421  dvcmulf  21422  fta1blem  21643  plyeq0lem  21681  coemulc  21725  dgreq0  21735  dgrmulc  21741  qaa  21792  dchrisumlema  22740  gx1  23752  gxnn0suc  23754  ofcc  26551  ofcof  26552  sseqf  26778  sseqp1  26781  cvmlift3lem9  27219  prodf1  27409  prod0  27459  fprodconst  27492  ismrer1  28740  stoweidlem21  29819  stoweidlem47  29845  zlmodzxzscm  30757  coe1fzgsumd  30841  pmatcollpw1id  30902
  Copyright terms: Public domain W3C validator