Theorem fvconst2g 6467

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

Step	Hyp	Ref	Expression
1		fconstg 6092	. 2 |- ( B e. D -> ( A X. { B } ) : A --> { B } )
2		fvconst 6431	. 2 |- ( ( ( A X. { B } ) : A --> { B } /\ C e. A ) -> ( ( A X. { B } ) ` C ) = B )
3	1, 2	sylan 488	1 |- ( ( B e. D /\ C e. A ) -> ( ( A X. { B } ) ` C ) = B )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   {csn 4177   X. cxp 5112   -->wf 5884   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896

This theorem is referenced by:  fconst2g  6468  fvconst2  6469  ofc1  6920  ofc2  6921  caofid0l  6925  caofid0r  6926  caofid1  6927  caofid2  6928  fnsuppres  7322  ser0  12853  ser1const  12857  exp1  12866  expp1  12867  climconst2  14279  climaddc1  14365  climmulc2  14367  climsubc1  14368  climsubc2  14369  climlec2  14389  fsumconst  14522  supcvg  14588  prodf1  14623  prod0  14673  fprodconst  14708  seq1st  15284  algr0  15285  algrf  15286  ramz  15729  pwsbas  16147  pwsplusgval  16150  pwsmulrval  16151  pwsle  16152  pwsvscafval  16154  pwspjmhm  17368  pwsco1mhm  17370  pwsinvg  17528  mulg1  17548  mulgnnp1  17549  mulgnnsubcl  17553  mulgnn0z  17567  mulgnndir  17569  mulgnndirOLD  17570  mulgnn0di  18231  gsumconst  18334  pwslmod  18970  psrlidm  19403  coe1tm  19643  coe1fzgsumd  19672  evl1scad  19699  frlmvscaval  20110  decpmatid  20575  pmatcollpwscmatlem1  20594  lmconst  21065  cnconst2  21087  xkoptsub  21457  xkopt  21458  xkopjcn  21459  tmdgsum  21899  tmdgsum2  21900  symgtgp  21905  cstucnd  22088  pcoptcl  22821  pcopt  22822  pcopt2  22823  dvidlem  23679  dvconst  23680  dvnff  23686  dvn0  23687  dvcmul  23707  dvcmulf  23708  fta1blem  23928  plyeq0lem  23966  coemulc  24011  dgreq0  24021  dgrmulc  24027  qaa  24078  dchrisumlema  25177  ofcc  30168  ofcof  30169  sseqf  30454  sseqp1  30457  cvmlift3lem9  31309  ismrer1  33637  dvsinax  40127  stoweidlem21  40238  stoweidlem47  40264  elaa2  40451  zlmodzxzscm  42135