Theorem fvconst2g 7194

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {csn 4601   × cxp 5652  ⟶wf 6527  ‘cfv 6531

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539

This theorem is referenced by:  fconst2g  7195  fvconst2  7196  ofc1  7699  ofc2  7700  caofid0l  7704  caofid0r  7705  caofid1  7706  caofid2  7707  fnsuppres  8190  ser0  14072  ser1const  14076  exp1  14085  expp1  14086  climconst2  15564  climaddc1  15651  climmulc2  15653  climsubc1  15654  climsubc2  15655  climlec2  15675  fsumconst  15806  supcvg  15872  prodf1  15907  prod0  15959  fprodconst  15994  seq1st  16590  algr0  16591  algrf  16592  ramz  17045  pwsbas  17501  pwsplusgval  17504  pwsmulrval  17505  pwsle  17506  pwsvscafval  17508  pwspjmhm  18808  pwsco1mhm  18810  pwsinvg  19036  mulgnngsum  19062  mulg1  19064  mulgnnp1  19065  mulgnnsubcl  19069  mulgnn0z  19084  mulgnndir  19086  mulgnn0di  19806  gsumconst  19915  pwslmod  20927  frlmvscaval  21728  psrlidm  21922  psrascl  21939  coe1tm  22210  coe1fzgsumd  22242  evl1scad  22273  evls1scafv  22304  decpmatid  22708  pmatcollpwscmatlem1  22727  lmconst  23199  cnconst2  23221  xkoptsub  23592  xkopt  23593  xkopjcn  23594  tmdgsum  24033  tmdgsum2  24034  symgtgp  24044  cstucnd  24222  pcoptcl  24972  pcopt  24973  pcopt2  24974  dvidlem  25868  dvconst  25870  dvnff  25877  dvn0  25878  dvcmul  25899  dvcmulf  25900  fta1blem  26128  plyeq0lem  26167  coemulc  26212  dgreq0  26223  dgrmulc  26229  qaa  26283  dchrisumlema  27451  exps1  28366  expsp1  28367  suppovss  32658  fdifsuppconst  32666  ofcc  34137  ofcof  34138  sseqf  34424  sseqp1  34427  lpadleft  34715  cvmlift3lem9  35349  ismrer1  37862  frlmvscadiccat  42529  evlsscaval  42587  fsuppssind  42616  ofoafo  43380  ofoaid1  43382  ofoaid2  43383  naddcnffo  43388  naddcnfid1  43391  dvsinax  45942  stoweidlem21  46050  stoweidlem47  46076  elaa2  46263  zlmodzxzscm  48332  2sphere0  48730  fvconstr  48838  fvconstrn0  48839