Theorem fvconst2g 6956

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 6552	. 2 ⊢ (𝐵 ∈ 𝐷 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2		fvconst 6918	. 2 ⊢ (((𝐴 × {𝐵}):𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)
3	1, 2	sylan 584	1 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112  {csn 4523   × cxp 5523  ⟶wf 6332  ‘cfv 6336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-v 3412  df-sbc 3698  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-fv 6344

This theorem is referenced by:  fconst2g  6957  fvconst2  6958  ofc1  7431  ofc2  7432  caofid0l  7436  caofid0r  7437  caofid1  7438  caofid2  7439  fnsuppres  7866  ser0  13465  ser1const  13469  exp1  13478  expp1  13479  climconst2  14946  climaddc1  15032  climmulc2  15034  climsubc1  15035  climsubc2  15036  climlec2  15056  fsumconst  15186  supcvg  15252  prodf1  15288  prod0  15338  fprodconst  15373  seq1st  15960  algr0  15961  algrf  15962  ramz  16409  pwsbas  16811  pwsplusgval  16814  pwsmulrval  16815  pwsle  16816  pwsvscafval  16818  pwspjmhm  18053  pwsco1mhm  18055  pwsinvg  18272  mulgnngsum  18293  mulg1  18295  mulgnnp1  18296  mulgnnsubcl  18300  mulgnn0z  18314  mulgnndir  18316  mulgnn0di  19007  gsumconst  19115  pwslmod  19803  frlmvscaval  20526  psrlidm  20724  coe1tm  20990  coe1fzgsumd  21019  evl1scad  21047  decpmatid  21463  pmatcollpwscmatlem1  21482  lmconst  21954  cnconst2  21976  xkoptsub  22347  xkopt  22348  xkopjcn  22349  tmdgsum  22788  tmdgsum2  22789  symgtgp  22799  cstucnd  22978  pcoptcl  23715  pcopt  23716  pcopt2  23717  dvidlem  24607  dvconst  24609  dvnff  24615  dvn0  24616  dvcmul  24636  dvcmulf  24637  fta1blem  24861  plyeq0lem  24899  coemulc  24944  dgreq0  24954  dgrmulc  24960  qaa  25011  dchrisumlema  26164  suppovss  30534  fdifsuppconst  30540  ofcc  31586  ofcof  31587  sseqf  31871  sseqp1  31874  lpadleft  32175  cvmlift3lem9  32798  ismrer1  35549  frlmvscadiccat  39737  evlsscaval  39771  fsuppssind  39780  mhphf  39783  dvsinax  42914  stoweidlem21  43022  stoweidlem47  43048  elaa2  43235  zlmodzxzscm  45119  2sphere0  45522