Theorem fvconst2g 7150

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {csn 4568   × cxp 5622  ⟶wf 6488  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500

This theorem is referenced by:  fconst2g  7151  fvconst2  7152  ofc1  7652  ofc2  7653  caofid0l  7657  caofid0r  7658  caofid1  7659  caofid2  7660  fnsuppres  8134  ser0  14007  ser1const  14011  exp1  14020  expp1  14021  climconst2  15501  climaddc1  15588  climmulc2  15590  climsubc1  15591  climsubc2  15592  climlec2  15612  fsumconst  15743  supcvg  15812  prodf1  15847  prod0  15899  fprodconst  15934  seq1st  16531  algr0  16532  algrf  16533  ramz  16987  pwsbas  17441  pwsplusgval  17445  pwsmulrval  17446  pwsle  17447  pwsvscafval  17449  pwspjmhm  18789  pwsco1mhm  18791  pwsinvg  19020  mulgnngsum  19046  mulg1  19048  mulgnnp1  19049  mulgnnsubcl  19053  mulgnn0z  19068  mulgnndir  19070  mulgnn0di  19791  gsumconst  19900  pwslmod  20956  frlmvscaval  21758  psrlidm  21950  psrascl  21967  coe1tm  22248  coe1fzgsumd  22279  evl1scad  22310  evls1scafv  22341  decpmatid  22745  pmatcollpwscmatlem1  22764  lmconst  23236  cnconst2  23258  xkoptsub  23629  xkopt  23630  xkopjcn  23631  tmdgsum  24070  tmdgsum2  24071  symgtgp  24081  cstucnd  24258  pcoptcl  24998  pcopt  24999  pcopt2  25000  dvidlem  25892  dvconst  25894  dvnff  25900  dvn0  25901  dvcmul  25921  dvcmulf  25922  fta1blem  26146  plyeq0lem  26185  coemulc  26230  dgreq0  26240  dgrmulc  26246  qaa  26300  dchrisumlema  27465  exps1  28434  expsp1  28435  constcof  32709  suppovss  32769  fdifsuppconst  32777  evlscaval  33699  ofcc  34266  ofcof  34267  sseqf  34552  sseqp1  34555  lpadleft  34843  cvmlift3lem9  35525  ismrer1  38173  frlmvscadiccat  42965  evlsscaval  43014  fsuppssind  43040  ofoafo  43802  ofoaid1  43804  ofoaid2  43805  naddcnffo  43810  naddcnfid1  43813  dvsinax  46359  stoweidlem21  46467  stoweidlem47  46493  elaa2  46680  zlmodzxzscm  48845  2sphere0  49238  fvconstr  49349  fvconstrn0  49350