Theorem fvconst2g 7222

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {csn 4626   × cxp 5683  ⟶wf 6557  ‘cfv 6561

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569

This theorem is referenced by:  fconst2g  7223  fvconst2  7224  ofc1  7725  ofc2  7726  caofid0l  7730  caofid0r  7731  caofid1  7732  caofid2  7733  fnsuppres  8216  ser0  14095  ser1const  14099  exp1  14108  expp1  14109  climconst2  15584  climaddc1  15671  climmulc2  15673  climsubc1  15674  climsubc2  15675  climlec2  15695  fsumconst  15826  supcvg  15892  prodf1  15927  prod0  15979  fprodconst  16014  seq1st  16608  algr0  16609  algrf  16610  ramz  17063  pwsbas  17532  pwsplusgval  17535  pwsmulrval  17536  pwsle  17537  pwsvscafval  17539  pwspjmhm  18843  pwsco1mhm  18845  pwsinvg  19071  mulgnngsum  19097  mulg1  19099  mulgnnp1  19100  mulgnnsubcl  19104  mulgnn0z  19119  mulgnndir  19121  mulgnn0di  19843  gsumconst  19952  pwslmod  20968  frlmvscaval  21788  psrlidm  21982  psrascl  21999  coe1tm  22276  coe1fzgsumd  22308  evl1scad  22339  evls1scafv  22370  decpmatid  22776  pmatcollpwscmatlem1  22795  lmconst  23269  cnconst2  23291  xkoptsub  23662  xkopt  23663  xkopjcn  23664  tmdgsum  24103  tmdgsum2  24104  symgtgp  24114  cstucnd  24293  pcoptcl  25054  pcopt  25055  pcopt2  25056  dvidlem  25950  dvconst  25952  dvnff  25959  dvn0  25960  dvcmul  25981  dvcmulf  25982  fta1blem  26210  plyeq0lem  26249  coemulc  26294  dgreq0  26305  dgrmulc  26311  qaa  26365  dchrisumlema  27532  exps1  28411  expsp1  28412  suppovss  32690  fdifsuppconst  32698  ofcc  34107  ofcof  34108  sseqf  34394  sseqp1  34397  lpadleft  34698  cvmlift3lem9  35332  ismrer1  37845  frlmvscadiccat  42516  evlsscaval  42574  fsuppssind  42603  ofoafo  43369  ofoaid1  43371  ofoaid2  43372  naddcnffo  43377  naddcnfid1  43380  dvsinax  45928  stoweidlem21  46036  stoweidlem47  46062  elaa2  46249  zlmodzxzscm  48273  2sphere0  48671  fvconstr  48765  fvconstrn0  48766