Theorem fvconst2 6469

Description: The value of a constant function. (Contributed by NM, 16-Apr-2005.)

Hypothesis

Ref	Expression
fvconst2.1	|- B e. _V

Assertion

Ref	Expression
fvconst2	|- ( C e. A -> ( ( A X. { B } ) ` C ) = B )

Proof of Theorem fvconst2

Step	Hyp	Ref	Expression
1		fvconst2.1	. 2 |- B e. _V
2		fvconst2g 6467	. 2 |- ( ( B e. _V /\ C e. A ) -> ( ( A X. { B } ) ` C ) = B )
3	1, 2	mpan 706	1 |- ( C e. A -> ( ( A X. { B } ) ` C ) = B )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   _Vcvv 3200   {csn 4177   X. cxp 5112   ` 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:  ovconst2  6814  mapsncnv  7904  ofsubeq0  11017  ofsubge0  11019  ser0f  12854  hashinf  13122  iserge0  14391  iseraltlem1  14412  sum0  14452  sumz  14453  harmonic  14591  prodf1f  14624  fprodntriv  14672  prod1  14674  setcmon  16737  0mhm  17358  mulgpropd  17584  dprdsubg  18423  0lmhm  19040  mplsubglem  19434  coe1tm  19643  frlmlmod  20093  frlmlss  20095  frlmbas  20099  frlmip  20117  islindf4  20177  mdetuni0  20427  txkgen  21455  xkofvcn  21487  nmo0  22539  pcorevlem  22826  rrxip  23178  mbfpos  23418  0pval  23438  0pledm  23440  xrge0f  23498  itg2ge0  23502  ibl0  23553  bddibl  23606  dvcmul  23707  dvef  23743  rolle  23753  dveq0  23763  dv11cn  23764  ftc2  23807  tdeglem4  23820  ply1rem  23923  fta1g  23927  fta1blem  23928  0dgrb  24002  dgrnznn  24003  dgrlt  24022  plymul0or  24036  plydivlem4  24051  plyrem  24060  fta1  24063  vieta1lem2  24066  elqaalem3  24076  aaliou2  24095  ulmdvlem1  24154  dchrelbas2  24962  dchrisumlem3  25180  axlowdimlem9  25830  axlowdimlem12  25833  axlowdimlem17  25838  0oval  27643  occllem  28162  ho01i  28687  0cnfn  28839  0lnfn  28844  nmfn0  28846  nlelchi  28920  opsqrlem2  29000  opsqrlem4  29002  opsqrlem5  29003  hmopidmchi  29010  breprexpnat  30712  circlemethnat  30719  circlevma  30720  connpconn  31217  txsconnlem  31222  cvxsconn  31225  cvmliftphtlem  31299  noetalem3  31865  fullfunfv  32054  matunitlindflem1  33405  matunitlindflem2  33406  ptrecube  33409  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem23  33432  poimirlem28  33437  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  poimir  33442  broucube  33443  mblfinlem2  33447  itg2addnclem  33461  itg2addnc  33464  ftc1anclem5  33489  ftc2nc  33494  cnpwstotbnd  33596  lfl0f  34356  eqlkr2  34387  lcd0vvalN  36902  mzpsubst  37311  mzpcompact2lem  37314  mzpcong  37539  hbtlem2  37694  mncn0  37709  mpaaeu  37720  aaitgo  37732  rngunsnply  37743  hashnzfzclim  38521  ofsubid  38523  dvconstbi  38533  binomcxplemnotnn0  38555  n0p  39209  snelmap  39254  aacllem  42547