Theorem fvconst2g 7153

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {csn 4562   × cxp 5623  ⟶wf 6488  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500

This theorem is referenced by:  fconst2g  7154  fvconst2  7155  ofc1  7655  ofc2  7656  caofid0l  7660  caofid0r  7661  caofid1  7662  caofid2  7663  fnsuppres  8138  ser0  14014  ser1const  14018  exp1  14027  expp1  14028  climconst2  15508  climaddc1  15595  climmulc2  15597  climsubc1  15598  climsubc2  15599  climlec2  15619  fsumconst  15750  supcvg  15819  prodf1  15854  prod0  15906  fprodconst  15941  seq1st  16538  algr0  16539  algrf  16540  ramz  16994  pwsbas  17448  pwsplusgval  17452  pwsmulrval  17453  pwsle  17454  pwsvscafval  17456  pwspjmhm  18796  pwsco1mhm  18798  pwsinvg  19027  mulgnngsum  19053  mulg1  19055  mulgnnp1  19056  mulgnnsubcl  19060  mulgnn0z  19075  mulgnndir  19077  mulgnn0di  19798  gsumconst  19907  pwslmod  20967  frlmvscaval  21750  psrlidm  21943  psrascl  21960  evlsscaval  22109  coe1tm  22266  coe1fzgsumd  22297  evl1scad  22328  evls1scafv  22359  decpmatid  22760  pmatcollpwscmatlem1  22779  lmconst  23251  cnconst2  23273  xkoptsub  23644  xkopt  23645  xkopjcn  23646  tmdgsum  24085  tmdgsum2  24086  symgtgp  24096  cstucnd  24273  pcoptcl  25013  pcopt  25014  pcopt2  25015  dvidlem  25907  dvconst  25909  dvnff  25915  dvn0  25916  dvcmul  25936  dvcmulf  25937  fta1blem  26161  plyeq0lem  26200  coemulc  26245  dgreq0  26255  dgrmulc  26261  qaa  26314  dchrisumlema  27476  exps1  28445  expsp1  28446  constcof  32720  suppovss  32780  fdifsuppconst  32788  evlscaval  33731  ofcc  34297  ofcof  34298  sseqf  34583  sseqp1  34586  lpadleft  34874  cvmlift3lem9  35562  ismrer1  38212  frlmvscadiccat  43003  fsuppssind  43050  ofoafo  43808  ofoaid1  43810  ofoaid2  43811  naddcnffo  43816  naddcnfid1  43819  dvsinax  46363  stoweidlem21  46471  stoweidlem47  46497  elaa2  46684  zlmodzxzscm  48855  2sphere0  49248  fvconstr  49359  fvconstrn0  49360