Theorem fvconst2g 5920

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 5584	. 2 |- ( B e. D -> ( A X. { B } ) : A --> { B } )
2		fvconst 5894	. 2 |- ( ( ( A X. { B } ) : A --> { B } /\ C e. A ) -> ( ( A X. { B } ) ` C ) = B )
3	1, 2	sylan 283	1 |- ( ( B e. D /\ C e. A ) -> ( ( A X. { B } ) ` C ) = B )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209   {csn 3705   X. cxp 4767   -->wf 5368   ` cfv 5372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4244  ax-pow 4306  ax-pr 4341

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-opab 4188  df-mpt 4189  df-id 4433  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-rn 4780  df-iota 5332  df-fun 5374  df-fn 5375  df-f 5376  df-fv 5380

This theorem is referenced by:  fconst2g  5921  fvconst2  5922  ofc1g  6314  ofc2g  6315  caofid0l  6319  caofid0r  6320  caofid1  6321  caofid2  6322  fczsupp0  6489  ser0  10948  exp3vallem  10955  exp3val  10956  exp1  10960  expp1  10961  resqrexlem1arp  11749  resqrexlemf1  11752  climconst2  12035  climaddc1  12073  climmulc2  12075  climsubc1  12076  climsubc2  12077  climlec2  12085  prodf1  12287  prod0  12330  ialgrlemconst  12799  ialgr0  12800  algrf  12801  algrp1  12802  0mhm  13770  mulgval  13902  mulgfng  13904  mulgnngzsum  13907  mulg1  13909  mulgnnp1  13910  mulgnnsubcl  13914  mulgnn0z  13929  mulgnndir  13931  gsumconstcmn  14143  pwsbas  14182  pwsplusgval  14185  pwsmulrval  14186  pwsinvg  14192  mplsubgfilemm  15012  lmconst  15240  cnconst2  15257  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvconst  15718  dvconstre  15720  dvconstss  15722  dvef  15751