Theorem fvconst2g 7071

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2109  {csn 4566   × cxp 5586  ⟶wf 6426  ‘cfv 6430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-fv 6438

This theorem is referenced by:  fconst2g  7072  fvconst2  7073  ofc1  7550  ofc2  7551  caofid0l  7555  caofid0r  7556  caofid1  7557  caofid2  7558  fnsuppres  7991  ser0  13756  ser1const  13760  exp1  13769  expp1  13770  climconst2  15238  climaddc1  15325  climmulc2  15327  climsubc1  15328  climsubc2  15329  climlec2  15351  fsumconst  15483  supcvg  15549  prodf1  15584  prod0  15634  fprodconst  15669  seq1st  16257  algr0  16258  algrf  16259  ramz  16707  pwsbas  17179  pwsplusgval  17182  pwsmulrval  17183  pwsle  17184  pwsvscafval  17186  pwspjmhm  18449  pwsco1mhm  18451  pwsinvg  18669  mulgnngsum  18690  mulg1  18692  mulgnnp1  18693  mulgnnsubcl  18697  mulgnn0z  18711  mulgnndir  18713  mulgnn0di  19408  gsumconst  19516  pwslmod  20213  frlmvscaval  20956  psrlidm  21153  coe1tm  21425  coe1fzgsumd  21454  evl1scad  21482  decpmatid  21900  pmatcollpwscmatlem1  21919  lmconst  22393  cnconst2  22415  xkoptsub  22786  xkopt  22787  xkopjcn  22788  tmdgsum  23227  tmdgsum2  23228  symgtgp  23238  cstucnd  23417  pcoptcl  24165  pcopt  24166  pcopt2  24167  dvidlem  25060  dvconst  25062  dvnff  25068  dvn0  25069  dvcmul  25089  dvcmulf  25090  fta1blem  25314  plyeq0lem  25352  coemulc  25397  dgreq0  25407  dgrmulc  25413  qaa  25464  dchrisumlema  26617  suppovss  30996  fdifsuppconst  31002  ofcc  32053  ofcof  32054  sseqf  32338  sseqp1  32341  lpadleft  32642  cvmlift3lem9  33268  ismrer1  35975  frlmvscadiccat  40217  evlsscaval  40253  fsuppssind  40262  mhphf  40265  dvsinax  43408  stoweidlem21  43516  stoweidlem47  43542  elaa2  43729  zlmodzxzscm  45645  2sphere0  46048  fvconstr  46135  fvconstrn0  46136