Theorem fvconst2g 7109

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

Assertion

Ref	Expression
fvconst2g	⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Proof of Theorem fvconst2g

Step	Hyp	Ref	Expression
1		fconstg 6691	. 2 ⊢ (𝐵 ∈ 𝐷 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2		fvconst 7068	. 2 ⊢ (((𝐴 × {𝐵}):𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
3	1, 2	sylan 581	1 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1539   ∈ wcel 2104  {csn 4565   × cxp 5598  ⟶wf 6454  ‘cfv 6458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-fv 6466

This theorem is referenced by:  fconst2g  7110  fvconst2  7111  ofc1  7591  ofc2  7592  caofid0l  7596  caofid0r  7597  caofid1  7598  caofid2  7599  fnsuppres  8038  ser0  13821  ser1const  13825  exp1  13834  expp1  13835  climconst2  15302  climaddc1  15389  climmulc2  15391  climsubc1  15392  climsubc2  15393  climlec2  15415  fsumconst  15547  supcvg  15613  prodf1  15648  prod0  15698  fprodconst  15733  seq1st  16321  algr0  16322  algrf  16323  ramz  16771  pwsbas  17243  pwsplusgval  17246  pwsmulrval  17247  pwsle  17248  pwsvscafval  17250  pwspjmhm  18513  pwsco1mhm  18515  pwsinvg  18733  mulgnngsum  18754  mulg1  18756  mulgnnp1  18757  mulgnnsubcl  18761  mulgnn0z  18775  mulgnndir  18777  mulgnn0di  19472  gsumconst  19580  pwslmod  20277  frlmvscaval  21020  psrlidm  21217  coe1tm  21489  coe1fzgsumd  21518  evl1scad  21546  decpmatid  21964  pmatcollpwscmatlem1  21983  lmconst  22457  cnconst2  22479  xkoptsub  22850  xkopt  22851  xkopjcn  22852  tmdgsum  23291  tmdgsum2  23292  symgtgp  23302  cstucnd  23481  pcoptcl  24229  pcopt  24230  pcopt2  24231  dvidlem  25124  dvconst  25126  dvnff  25132  dvn0  25133  dvcmul  25153  dvcmulf  25154  fta1blem  25378  plyeq0lem  25416  coemulc  25461  dgreq0  25471  dgrmulc  25477  qaa  25528  dchrisumlema  26681  suppovss  31062  fdifsuppconst  31068  ofcc  32119  ofcof  32120  sseqf  32404  sseqp1  32407  lpadleft  32708  cvmlift3lem9  33334  ismrer1  36040  frlmvscadiccat  40274  evlsscaval  40310  fsuppssind  40319  mhphf  40322  dvsinax  43503  stoweidlem21  43611  stoweidlem47  43637  elaa2  43824  zlmodzxzscm  45751  2sphere0  46154  fvconstr  46241  fvconstrn0  46242