Theorem fvconst2g 6966

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {csn 4569   × cxp 5555  ⟶wf 6353  ‘cfv 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-fv 6365

This theorem is referenced by:  fconst2g  6967  fvconst2  6968  ofc1  7434  ofc2  7435  caofid0l  7439  caofid0r  7440  caofid1  7441  caofid2  7442  fnsuppres  7859  ser0  13425  ser1const  13429  exp1  13438  expp1  13439  climconst2  14907  climaddc1  14993  climmulc2  14995  climsubc1  14996  climsubc2  14997  climlec2  15017  fsumconst  15147  supcvg  15213  prodf1  15249  prod0  15299  fprodconst  15334  seq1st  15917  algr0  15918  algrf  15919  ramz  16363  pwsbas  16762  pwsplusgval  16765  pwsmulrval  16766  pwsle  16767  pwsvscafval  16769  pwspjmhm  17996  pwsco1mhm  17998  pwsinvg  18214  mulgnngsum  18235  mulg1  18237  mulgnnp1  18238  mulgnnsubcl  18242  mulgnn0z  18256  mulgnndir  18258  mulgnn0di  18948  gsumconst  19056  pwslmod  19744  psrlidm  20185  coe1tm  20443  coe1fzgsumd  20472  evl1scad  20500  frlmvscaval  20914  decpmatid  21380  pmatcollpwscmatlem1  21399  lmconst  21871  cnconst2  21893  xkoptsub  22264  xkopt  22265  xkopjcn  22266  tmdgsum  22705  tmdgsum2  22706  symgtgp  22716  cstucnd  22895  pcoptcl  23627  pcopt  23628  pcopt2  23629  dvidlem  24515  dvconst  24516  dvnff  24522  dvn0  24523  dvcmul  24543  dvcmulf  24544  fta1blem  24764  plyeq0lem  24802  coemulc  24847  dgreq0  24857  dgrmulc  24863  qaa  24914  dchrisumlema  26066  suppovss  30428  ofcc  31367  ofcof  31368  sseqf  31652  sseqp1  31655  lpadleft  31956  cvmlift3lem9  32576  ismrer1  35118  frlmvscadiccat  39152  dvsinax  42204  stoweidlem21  42313  stoweidlem47  42339  elaa2  42526  zlmodzxzscm  44412  2sphere0  44744