Theorem fvconst2g 7146

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {csn 4555   × cxp 5616  ⟶wf 6481  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493

This theorem is referenced by:  fconst2g  7147  fvconst2  7148  ofc1  7648  ofc2  7649  caofid0l  7653  caofid0r  7654  caofid1  7655  caofid2  7656  fnsuppres  8131  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  20960  frlmvscaval  21743  psrlidm  21936  psrascl  21953  evlsscaval  22102  coe1tm  22259  coe1fzgsumd  22290  evl1scad  22321  evls1scafv  22352  decpmatid  22753  pmatcollpwscmatlem1  22772  lmconst  23244  cnconst2  23266  xkoptsub  23637  xkopt  23638  xkopjcn  23639  tmdgsum  24078  tmdgsum2  24079  symgtgp  24089  cstucnd  24266  pcoptcl  25006  pcopt  25007  pcopt2  25008  dvidlem  25900  dvconst  25902  dvnff  25908  dvn0  25909  dvcmul  25929  dvcmulf  25930  fta1blem  26154  plyeq0lem  26193  coemulc  26238  dgreq0  26248  dgrmulc  26254  qaa  26307  dchrisumlema  27469  exps1  28438  expsp1  28439  constcof  32713  suppovss  32773  fdifsuppconst  32781  evlscaval  33724  ofcc  34290  ofcof  34291  sseqf  34576  sseqp1  34579  lpadleft  34867  cvmlift3lem9  35555  ismrer1  38205  frlmvscadiccat  42996  fsuppssind  43043  ofoafo  43801  ofoaid1  43803  ofoaid2  43804  naddcnffo  43809  naddcnfid1  43812  dvsinax  46356  stoweidlem21  46464  stoweidlem47  46490  elaa2  46677  zlmodzxzscm  48848  2sphere0  49241  fvconstr  49352  fvconstrn0  49353