Theorem fvconst2g 7208

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {csn 4584   × cxp 5648  ⟶wf 6534  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546

This theorem is used by:  fconst2g  7209  fvconst2  7210  ofc1  7721  ofc2  7722  caofid0l  7726  caofid0r  7727  caofid1  7728  caofid2  7729  fnsuppres  8211  ser0  14200  ser1const  14204  exp1  14213  expp1  14214  climconst2  15720  climaddc1  15807  climmulc2  15809  climsubc1  15810  climsubc2  15811  climlec2  15831  fsumconst  15961  supcvg  16030  prodf1  16065  prod0  16115  fprodconst  16150  seq1st  16751  algr0  16752  algrf  16753  ramz  17208  pwsbas  17663  pwsplusgval  17667  pwsmulrval  17668  pwsle  17669  pwsvscafval  17671  pwspjmhm  19031  pwsco1mhm  19033  pwsinvg  19268  mulgnngsum  19294  mulg1  19296  mulgnnp1  19297  mulgnnsubcl  19301  mulgnn0z  19316  mulgnndir  19318  mulgnn0di  20044  gsumconst  20153  pwslmod  21250  frlmvscaval  22079  psrlidm  22274  psrascl  22291  evlsscaval  22440  coe1tm  22597  coe1fzgsumd  22627  evl1scad  22658  evls1scafv  22689  decpmatid  23093  pmatcollpwscmatlem1  23112  lmconst  23584  cnconst2  23606  xkoptsub  23978  xkopt  23979  xkopjcn  23980  tmdgsum  24419  tmdgsum2  24420  symgtgp  24430  cstucnd  24607  pcoptcl  25347  pcopt  25348  pcopt2  25349  dvidlem  26240  dvconst  26242  dvnff  26248  dvn0  26249  dvcmul  26269  dvcmulf  26270  fta1blem  26494  plyeq0lem  26534  coemulc  26579  dgreq0  26589  dgrmulc  26595  qaa  26652  dchrisumlema  27820  exps1  28819  expsp1  28820  constcof  33262  suppovss  33321  fdifsuppconst  33329  evlscaval  34218  ofcc  34784  ofcof  34785  sseqf  35070  sseqp1  35073  lpadleft  35361  cvmlift3lem9  36178  ismrer1  38865  frlmvscadiccat  43666  fsuppssind  43714  ofoafo  44451  ofoaid1  44453  ofoaid2  44454  naddcnffo  44459  naddcnfid1  44462  dvsinax  47016  stoweidlem21  47124  stoweidlem47  47150  elaa2  47337  sqrtnnaa  48006  sqrtnzqaa  48007  zlmodzxzscm  49562  2sphere0  49955  ovconstbrd  50066  ovconstbrn0d  50067