Theorem fvconst2g 7221

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {csn 4630   × cxp 5686  ⟶wf 6558  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570

This theorem is referenced by:  fconst2g  7222  fvconst2  7223  ofc1  7724  ofc2  7725  caofid0l  7729  caofid0r  7730  caofid1  7731  caofid2  7732  fnsuppres  8214  ser0  14091  ser1const  14095  exp1  14104  expp1  14105  climconst2  15580  climaddc1  15667  climmulc2  15669  climsubc1  15670  climsubc2  15671  climlec2  15691  fsumconst  15822  supcvg  15888  prodf1  15923  prod0  15975  fprodconst  16010  seq1st  16604  algr0  16605  algrf  16606  ramz  17058  pwsbas  17533  pwsplusgval  17536  pwsmulrval  17537  pwsle  17538  pwsvscafval  17540  pwspjmhm  18855  pwsco1mhm  18857  pwsinvg  19083  mulgnngsum  19109  mulg1  19111  mulgnnp1  19112  mulgnnsubcl  19116  mulgnn0z  19131  mulgnndir  19133  mulgnn0di  19857  gsumconst  19966  pwslmod  20985  frlmvscaval  21805  psrlidm  21999  psrascl  22016  coe1tm  22291  coe1fzgsumd  22323  evl1scad  22354  evls1scafv  22385  decpmatid  22791  pmatcollpwscmatlem1  22810  lmconst  23284  cnconst2  23306  xkoptsub  23677  xkopt  23678  xkopjcn  23679  tmdgsum  24118  tmdgsum2  24119  symgtgp  24129  cstucnd  24308  pcoptcl  25067  pcopt  25068  pcopt2  25069  dvidlem  25964  dvconst  25966  dvnff  25973  dvn0  25974  dvcmul  25995  dvcmulf  25996  fta1blem  26224  plyeq0lem  26263  coemulc  26308  dgreq0  26319  dgrmulc  26325  qaa  26379  dchrisumlema  27546  exps1  28425  expsp1  28426  suppovss  32695  fdifsuppconst  32703  ofcc  34086  ofcof  34087  sseqf  34373  sseqp1  34376  lpadleft  34676  cvmlift3lem9  35311  ismrer1  37824  frlmvscadiccat  42492  evlsscaval  42550  fsuppssind  42579  ofoafo  43345  ofoaid1  43347  ofoaid2  43348  naddcnffo  43353  naddcnfid1  43356  dvsinax  45868  stoweidlem21  45976  stoweidlem47  46002  elaa2  46189  zlmodzxzscm  48201  2sphere0  48599  fvconstr  48685  fvconstrn0  48686