Theorem fvconst2g 7136

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {csn 4576   × cxp 5614  ⟶wf 6477  ‘cfv 6481

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489

This theorem is referenced by:  fconst2g  7137  fvconst2  7138  ofc1  7638  ofc2  7639  caofid0l  7643  caofid0r  7644  caofid1  7645  caofid2  7646  fnsuppres  8121  ser0  13958  ser1const  13962  exp1  13971  expp1  13972  climconst2  15452  climaddc1  15539  climmulc2  15541  climsubc1  15542  climsubc2  15543  climlec2  15563  fsumconst  15694  supcvg  15760  prodf1  15795  prod0  15847  fprodconst  15882  seq1st  16479  algr0  16480  algrf  16481  ramz  16934  pwsbas  17388  pwsplusgval  17391  pwsmulrval  17392  pwsle  17393  pwsvscafval  17395  pwspjmhm  18735  pwsco1mhm  18737  pwsinvg  18963  mulgnngsum  18989  mulg1  18991  mulgnnp1  18992  mulgnnsubcl  18996  mulgnn0z  19011  mulgnndir  19013  mulgnn0di  19735  gsumconst  19844  pwslmod  20901  frlmvscaval  21703  psrlidm  21897  psrascl  21914  coe1tm  22185  coe1fzgsumd  22217  evl1scad  22248  evls1scafv  22279  decpmatid  22683  pmatcollpwscmatlem1  22702  lmconst  23174  cnconst2  23196  xkoptsub  23567  xkopt  23568  xkopjcn  23569  tmdgsum  24008  tmdgsum2  24009  symgtgp  24019  cstucnd  24196  pcoptcl  24946  pcopt  24947  pcopt2  24948  dvidlem  25841  dvconst  25843  dvnff  25850  dvn0  25851  dvcmul  25872  dvcmulf  25873  fta1blem  26101  plyeq0lem  26140  coemulc  26185  dgreq0  26196  dgrmulc  26202  qaa  26256  dchrisumlema  27424  exps1  28349  expsp1  28350  constcof  32599  suppovss  32657  fdifsuppconst  32665  ofcc  34114  ofcof  34115  sseqf  34400  sseqp1  34403  lpadleft  34691  cvmlift3lem9  35359  ismrer1  37877  frlmvscadiccat  42538  evlsscaval  42596  fsuppssind  42625  ofoafo  43388  ofoaid1  43390  ofoaid2  43391  naddcnffo  43396  naddcnfid1  43399  dvsinax  45950  stoweidlem21  46058  stoweidlem47  46084  elaa2  46271  zlmodzxzscm  48387  2sphere0  48781  fvconstr  48892  fvconstrn0  48893