Theorem fvconst2g 7179

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {csn 4592   × cxp 5639  ⟶wf 6510  ‘cfv 6514

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522

This theorem is referenced by:  fconst2g  7180  fvconst2  7181  ofc1  7684  ofc2  7685  caofid0l  7689  caofid0r  7690  caofid1  7691  caofid2  7692  fnsuppres  8173  ser0  14026  ser1const  14030  exp1  14039  expp1  14040  climconst2  15521  climaddc1  15608  climmulc2  15610  climsubc1  15611  climsubc2  15612  climlec2  15632  fsumconst  15763  supcvg  15829  prodf1  15864  prod0  15916  fprodconst  15951  seq1st  16548  algr0  16549  algrf  16550  ramz  17003  pwsbas  17457  pwsplusgval  17460  pwsmulrval  17461  pwsle  17462  pwsvscafval  17464  pwspjmhm  18764  pwsco1mhm  18766  pwsinvg  18992  mulgnngsum  19018  mulg1  19020  mulgnnp1  19021  mulgnnsubcl  19025  mulgnn0z  19040  mulgnndir  19042  mulgnn0di  19762  gsumconst  19871  pwslmod  20883  frlmvscaval  21684  psrlidm  21878  psrascl  21895  coe1tm  22166  coe1fzgsumd  22198  evl1scad  22229  evls1scafv  22260  decpmatid  22664  pmatcollpwscmatlem1  22683  lmconst  23155  cnconst2  23177  xkoptsub  23548  xkopt  23549  xkopjcn  23550  tmdgsum  23989  tmdgsum2  23990  symgtgp  24000  cstucnd  24178  pcoptcl  24928  pcopt  24929  pcopt2  24930  dvidlem  25823  dvconst  25825  dvnff  25832  dvn0  25833  dvcmul  25854  dvcmulf  25855  fta1blem  26083  plyeq0lem  26122  coemulc  26167  dgreq0  26178  dgrmulc  26184  qaa  26238  dchrisumlema  27406  exps1  28321  expsp1  28322  suppovss  32611  fdifsuppconst  32619  ofcc  34103  ofcof  34104  sseqf  34390  sseqp1  34393  lpadleft  34681  cvmlift3lem9  35321  ismrer1  37839  frlmvscadiccat  42501  evlsscaval  42559  fsuppssind  42588  ofoafo  43352  ofoaid1  43354  ofoaid2  43355  naddcnffo  43360  naddcnfid1  43363  dvsinax  45918  stoweidlem21  46026  stoweidlem47  46052  elaa2  46239  zlmodzxzscm  48349  2sphere0  48743  fvconstr  48854  fvconstrn0  48855