Theorem fvconst2g 7206

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105  {csn 4629   × cxp 5675  ⟶wf 6540  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552

This theorem is referenced by:  fconst2g  7207  fvconst2  7208  ofc1  7699  ofc2  7700  caofid0l  7704  caofid0r  7705  caofid1  7706  caofid2  7707  fnsuppres  8179  ser0  14025  ser1const  14029  exp1  14038  expp1  14039  climconst2  15497  climaddc1  15584  climmulc2  15586  climsubc1  15587  climsubc2  15588  climlec2  15610  fsumconst  15741  supcvg  15807  prodf1  15842  prod0  15892  fprodconst  15927  seq1st  16513  algr0  16514  algrf  16515  ramz  16963  pwsbas  17438  pwsplusgval  17441  pwsmulrval  17442  pwsle  17443  pwsvscafval  17445  pwspjmhm  18748  pwsco1mhm  18750  pwsinvg  18973  mulgnngsum  18996  mulg1  18998  mulgnnp1  18999  mulgnnsubcl  19003  mulgnn0z  19018  mulgnndir  19020  mulgnn0di  19735  gsumconst  19844  pwslmod  20726  frlmvscaval  21543  psrlidm  21743  coe1tm  22016  coe1fzgsumd  22047  evl1scad  22075  decpmatid  22493  pmatcollpwscmatlem1  22512  lmconst  22986  cnconst2  23008  xkoptsub  23379  xkopt  23380  xkopjcn  23381  tmdgsum  23820  tmdgsum2  23821  symgtgp  23831  cstucnd  24010  pcoptcl  24769  pcopt  24770  pcopt2  24771  dvidlem  25665  dvconst  25667  dvnff  25673  dvn0  25674  dvcmul  25694  dvcmulf  25695  fta1blem  25919  plyeq0lem  25957  coemulc  26002  dgreq0  26012  dgrmulc  26018  qaa  26069  dchrisumlema  27224  suppovss  32170  fdifsuppconst  32175  evls1scafv  32914  ofcc  33399  ofcof  33400  sseqf  33686  sseqp1  33689  lpadleft  33990  cvmlift3lem9  34613  ismrer1  37010  frlmvscadiccat  41387  evlsscaval  41439  fsuppssind  41468  ofoafo  42409  ofoaid1  42411  ofoaid2  42412  naddcnffo  42417  naddcnfid1  42420  dvsinax  44929  stoweidlem21  45037  stoweidlem47  45063  elaa2  45250  zlmodzxzscm  47123  2sphere0  47525  fvconstr  47611  fvconstrn0  47612