Theorem fvconst2g 7205

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {csn 4628   × cxp 5674  ⟶wf 6539  ‘cfv 6543

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551

This theorem is referenced by:  fconst2g  7206  fvconst2  7207  ofc1  7698  ofc2  7699  caofid0l  7703  caofid0r  7704  caofid1  7705  caofid2  7706  fnsuppres  8178  ser0  14022  ser1const  14026  exp1  14035  expp1  14036  climconst2  15494  climaddc1  15581  climmulc2  15583  climsubc1  15584  climsubc2  15585  climlec2  15607  fsumconst  15738  supcvg  15804  prodf1  15839  prod0  15889  fprodconst  15924  seq1st  16510  algr0  16511  algrf  16512  ramz  16960  pwsbas  17435  pwsplusgval  17438  pwsmulrval  17439  pwsle  17440  pwsvscafval  17442  pwspjmhm  18713  pwsco1mhm  18715  pwsinvg  18938  mulgnngsum  18961  mulg1  18963  mulgnnp1  18964  mulgnnsubcl  18968  mulgnn0z  18983  mulgnndir  18985  mulgnn0di  19695  gsumconst  19804  pwslmod  20586  frlmvscaval  21329  psrlidm  21529  coe1tm  21802  coe1fzgsumd  21833  evl1scad  21861  decpmatid  22279  pmatcollpwscmatlem1  22298  lmconst  22772  cnconst2  22794  xkoptsub  23165  xkopt  23166  xkopjcn  23167  tmdgsum  23606  tmdgsum2  23607  symgtgp  23617  cstucnd  23796  pcoptcl  24544  pcopt  24545  pcopt2  24546  dvidlem  25439  dvconst  25441  dvnff  25447  dvn0  25448  dvcmul  25468  dvcmulf  25469  fta1blem  25693  plyeq0lem  25731  coemulc  25776  dgreq0  25786  dgrmulc  25792  qaa  25843  dchrisumlema  26998  suppovss  31944  fdifsuppconst  31949  evls1scafv  32688  ofcc  33173  ofcof  33174  sseqf  33460  sseqp1  33463  lpadleft  33764  cvmlift3lem9  34387  ismrer1  36792  frlmvscadiccat  41166  evlsscaval  41218  fsuppssind  41247  ofoafo  42188  ofoaid1  42190  ofoaid2  42191  naddcnffo  42196  naddcnfid1  42199  dvsinax  44708  stoweidlem21  44816  stoweidlem47  44842  elaa2  45029  zlmodzxzscm  47112  2sphere0  47514  fvconstr  47600  fvconstrn0  47601