Theorem fvconst2g 7158

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {csn 4582   × cxp 5630  ⟶wf 6496  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508

This theorem is referenced by:  fconst2g  7159  fvconst2  7160  ofc1  7660  ofc2  7661  caofid0l  7665  caofid0r  7666  caofid1  7667  caofid2  7668  fnsuppres  8143  ser0  13989  ser1const  13993  exp1  14002  expp1  14003  climconst2  15483  climaddc1  15570  climmulc2  15572  climsubc1  15573  climsubc2  15574  climlec2  15594  fsumconst  15725  supcvg  15791  prodf1  15826  prod0  15878  fprodconst  15913  seq1st  16510  algr0  16511  algrf  16512  ramz  16965  pwsbas  17419  pwsplusgval  17423  pwsmulrval  17424  pwsle  17425  pwsvscafval  17427  pwspjmhm  18767  pwsco1mhm  18769  pwsinvg  18995  mulgnngsum  19021  mulg1  19023  mulgnnp1  19024  mulgnnsubcl  19028  mulgnn0z  19043  mulgnndir  19045  mulgnn0di  19766  gsumconst  19875  pwslmod  20933  frlmvscaval  21735  psrlidm  21929  psrascl  21946  coe1tm  22227  coe1fzgsumd  22260  evl1scad  22291  evls1scafv  22322  decpmatid  22726  pmatcollpwscmatlem1  22745  lmconst  23217  cnconst2  23239  xkoptsub  23610  xkopt  23611  xkopjcn  23612  tmdgsum  24051  tmdgsum2  24052  symgtgp  24062  cstucnd  24239  pcoptcl  24989  pcopt  24990  pcopt2  24991  dvidlem  25884  dvconst  25886  dvnff  25893  dvn0  25894  dvcmul  25915  dvcmulf  25916  fta1blem  26144  plyeq0lem  26183  coemulc  26228  dgreq0  26239  dgrmulc  26245  qaa  26299  dchrisumlema  27467  exps1  28436  expsp1  28437  constcof  32710  suppovss  32770  fdifsuppconst  32778  evlscaval  33716  ofcc  34283  ofcof  34284  sseqf  34569  sseqp1  34572  lpadleft  34860  cvmlift3lem9  35540  ismrer1  38083  frlmvscadiccat  42870  evlsscaval  42919  fsuppssind  42945  ofoafo  43707  ofoaid1  43709  ofoaid2  43710  naddcnffo  43715  naddcnfid1  43718  dvsinax  46265  stoweidlem21  46373  stoweidlem47  46399  elaa2  46586  zlmodzxzscm  48711  2sphere0  49104  fvconstr  49215  fvconstrn0  49216