Theorem fvconst2g 7190

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  {csn 4585   × cxp 5650  ⟶wf 6521  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fv 6533

This theorem is referenced by:  fconst2g  7191  fvconst2  7192  ofc1  7692  ofc2  7693  caofid0l  7697  caofid0r  7698  caofid1  7699  caofid2  7700  fnsuppres  8175  ser0  14081  ser1const  14085  exp1  14094  expp1  14095  climconst2  15589  climaddc1  15676  climmulc2  15678  climsubc1  15679  climsubc2  15680  climlec2  15700  fsumconst  15831  supcvg  15900  prodf1  15935  prod0  15987  fprodconst  16022  seq1st  16619  algr0  16620  algrf  16621  ramz  17075  pwsbas  17530  pwsplusgval  17534  pwsmulrval  17535  pwsle  17536  pwsvscafval  17538  pwspjmhm  18879  pwsco1mhm  18881  pwsinvg  19110  mulgnngsum  19136  mulg1  19138  mulgnnp1  19139  mulgnnsubcl  19143  mulgnn0z  19158  mulgnndir  19160  mulgnn0di  19886  gsumconst  19995  pwslmod  21060  frlmvscaval  21878  psrlidm  22071  psrascl  22088  evlsscaval  22237  coe1tm  22394  coe1fzgsumd  22425  evl1scad  22456  evls1scafv  22487  decpmatid  22888  pmatcollpwscmatlem1  22907  lmconst  23379  cnconst2  23401  xkoptsub  23772  xkopt  23773  xkopjcn  23774  tmdgsum  24213  tmdgsum2  24214  symgtgp  24224  cstucnd  24401  pcoptcl  25141  pcopt  25142  pcopt2  25143  dvidlem  26035  dvconst  26037  dvnff  26043  dvn0  26044  dvcmul  26064  dvcmulf  26065  fta1blem  26289  plyeq0lem  26328  coemulc  26373  dgreq0  26383  dgrmulc  26389  qaa  26445  dchrisumlema  27610  exps1  28579  expsp1  28580  constcof  32878  suppovss  32938  fdifsuppconst  32946  evlscaval  33847  ofcc  34413  ofcof  34414  sseqf  34699  sseqp1  34702  lpadleft  34990  cvmlift3lem9  35690  ismrer1  38349  frlmvscadiccat  43140  fsuppssind  43187  ofoafo  43945  ofoaid1  43947  ofoaid2  43948  naddcnffo  43953  naddcnfid1  43956  dvsinax  46485  stoweidlem21  46593  stoweidlem47  46619  elaa2  46806  zlmodzxzscm  48988  2sphere0  49381  fvconstr  49491  fvconstrn0  49492