Theorem fvconst2g 7176

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {csn 4589   × cxp 5636  ⟶wf 6507  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519

This theorem is referenced by:  fconst2g  7177  fvconst2  7178  ofc1  7681  ofc2  7682  caofid0l  7686  caofid0r  7687  caofid1  7688  caofid2  7689  fnsuppres  8170  ser0  14019  ser1const  14023  exp1  14032  expp1  14033  climconst2  15514  climaddc1  15601  climmulc2  15603  climsubc1  15604  climsubc2  15605  climlec2  15625  fsumconst  15756  supcvg  15822  prodf1  15857  prod0  15909  fprodconst  15944  seq1st  16541  algr0  16542  algrf  16543  ramz  16996  pwsbas  17450  pwsplusgval  17453  pwsmulrval  17454  pwsle  17455  pwsvscafval  17457  pwspjmhm  18757  pwsco1mhm  18759  pwsinvg  18985  mulgnngsum  19011  mulg1  19013  mulgnnp1  19014  mulgnnsubcl  19018  mulgnn0z  19033  mulgnndir  19035  mulgnn0di  19755  gsumconst  19864  pwslmod  20876  frlmvscaval  21677  psrlidm  21871  psrascl  21888  coe1tm  22159  coe1fzgsumd  22191  evl1scad  22222  evls1scafv  22253  decpmatid  22657  pmatcollpwscmatlem1  22676  lmconst  23148  cnconst2  23170  xkoptsub  23541  xkopt  23542  xkopjcn  23543  tmdgsum  23982  tmdgsum2  23983  symgtgp  23993  cstucnd  24171  pcoptcl  24921  pcopt  24922  pcopt2  24923  dvidlem  25816  dvconst  25818  dvnff  25825  dvn0  25826  dvcmul  25847  dvcmulf  25848  fta1blem  26076  plyeq0lem  26115  coemulc  26160  dgreq0  26171  dgrmulc  26177  qaa  26231  dchrisumlema  27399  exps1  28314  expsp1  28315  suppovss  32604  fdifsuppconst  32612  ofcc  34096  ofcof  34097  sseqf  34383  sseqp1  34386  lpadleft  34674  cvmlift3lem9  35314  ismrer1  37832  frlmvscadiccat  42494  evlsscaval  42552  fsuppssind  42581  ofoafo  43345  ofoaid1  43347  ofoaid2  43348  naddcnffo  43353  naddcnfid1  43356  dvsinax  45911  stoweidlem21  46019  stoweidlem47  46045  elaa2  46232  zlmodzxzscm  48345  2sphere0  48739  fvconstr  48850  fvconstrn0  48851