Theorem fvconst2g 7142

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {csn 4579   × cxp 5621  ⟶wf 6482  ‘cfv 6486

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 5238  ax-nul 5248  ax-pr 5374

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494

This theorem is referenced by:  fconst2g  7143  fvconst2  7144  ofc1  7645  ofc2  7646  caofid0l  7650  caofid0r  7651  caofid1  7652  caofid2  7653  fnsuppres  8131  ser0  13979  ser1const  13983  exp1  13992  expp1  13993  climconst2  15473  climaddc1  15560  climmulc2  15562  climsubc1  15563  climsubc2  15564  climlec2  15584  fsumconst  15715  supcvg  15781  prodf1  15816  prod0  15868  fprodconst  15903  seq1st  16500  algr0  16501  algrf  16502  ramz  16955  pwsbas  17409  pwsplusgval  17412  pwsmulrval  17413  pwsle  17414  pwsvscafval  17416  pwspjmhm  18722  pwsco1mhm  18724  pwsinvg  18950  mulgnngsum  18976  mulg1  18978  mulgnnp1  18979  mulgnnsubcl  18983  mulgnn0z  18998  mulgnndir  19000  mulgnn0di  19722  gsumconst  19831  pwslmod  20891  frlmvscaval  21693  psrlidm  21887  psrascl  21904  coe1tm  22175  coe1fzgsumd  22207  evl1scad  22238  evls1scafv  22269  decpmatid  22673  pmatcollpwscmatlem1  22692  lmconst  23164  cnconst2  23186  xkoptsub  23557  xkopt  23558  xkopjcn  23559  tmdgsum  23998  tmdgsum2  23999  symgtgp  24009  cstucnd  24187  pcoptcl  24937  pcopt  24938  pcopt2  24939  dvidlem  25832  dvconst  25834  dvnff  25841  dvn0  25842  dvcmul  25863  dvcmulf  25864  fta1blem  26092  plyeq0lem  26131  coemulc  26176  dgreq0  26187  dgrmulc  26193  qaa  26247  dchrisumlema  27415  exps1  28338  expsp1  28339  suppovss  32637  fdifsuppconst  32645  ofcc  34072  ofcof  34073  sseqf  34359  sseqp1  34362  lpadleft  34650  cvmlift3lem9  35299  ismrer1  37817  frlmvscadiccat  42479  evlsscaval  42537  fsuppssind  42566  ofoafo  43329  ofoaid1  43331  ofoaid2  43332  naddcnffo  43337  naddcnfid1  43340  dvsinax  45895  stoweidlem21  46003  stoweidlem47  46029  elaa2  46216  zlmodzxzscm  48342  2sphere0  48736  fvconstr  48847  fvconstrn0  48848