Theorem fvconst2g 6723

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

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1658   ∈ wcel 2166  {csn 4397   × cxp 5340  ⟶wf 6119  ‘cfv 6123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-fv 6131

This theorem is referenced by:  fconst2g  6724  fvconst2  6725  ofc1  7180  ofc2  7181  caofid0l  7185  caofid0r  7186  caofid1  7187  caofid2  7188  fnsuppres  7587  ser0  13147  ser1const  13151  exp1  13160  expp1  13161  climconst2  14656  climaddc1  14742  climmulc2  14744  climsubc1  14745  climsubc2  14746  climlec2  14766  fsumconst  14896  supcvg  14962  prodf1  14996  prod0  15046  fprodconst  15081  seq1st  15657  algr0  15658  algrf  15659  ramz  16100  pwsbas  16500  pwsplusgval  16503  pwsmulrval  16504  pwsle  16505  pwsvscafval  16507  pwspjmhm  17721  pwsco1mhm  17723  pwsinvg  17882  mulg1  17902  mulgnnp1  17903  mulgnnsubcl  17907  mulgnn0z  17920  mulgnndir  17922  mulgnn0di  18584  gsumconst  18687  pwslmod  19329  psrlidm  19764  coe1tm  20003  coe1fzgsumd  20032  evl1scad  20059  frlmvscaval  20474  decpmatid  20945  pmatcollpwscmatlem1  20964  lmconst  21436  cnconst2  21458  xkoptsub  21828  xkopt  21829  xkopjcn  21830  tmdgsum  22269  tmdgsum2  22270  symgtgp  22275  cstucnd  22458  pcoptcl  23190  pcopt  23191  pcopt2  23192  dvidlem  24078  dvconst  24079  dvnff  24085  dvn0  24086  dvcmul  24106  dvcmulf  24107  fta1blem  24327  plyeq0lem  24365  coemulc  24410  dgreq0  24420  dgrmulc  24426  qaa  24477  dchrisumlema  25590  ofcc  30713  ofcof  30714  sseqf  31000  sseqp1  31003  cvmlift3lem9  31855  ismrer1  34179  dvsinax  40922  stoweidlem21  41032  stoweidlem47  41058  elaa2  41245  zlmodzxzscm  42982  2sphere0  43302