Theorem fvconst2g 7202

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {csn 4590   × cxp 5661  ⟶wf 6534  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546

This theorem is referenced by:  fconst2g  7203  fvconst2  7204  ofc1  7704  ofc2  7705  caofid0l  7709  caofid0r  7710  caofid1  7711  caofid2  7712  fnsuppres  8188  ser0  14092  ser1const  14096  exp1  14105  expp1  14106  climconst2  15601  climaddc1  15688  climmulc2  15690  climsubc1  15691  climsubc2  15692  climlec2  15712  fsumconst  15843  supcvg  15912  prodf1  15947  prod0  15999  fprodconst  16034  seq1st  16630  algr0  16631  algrf  16632  ramz  17086  pwsbas  17541  pwsplusgval  17545  pwsmulrval  17546  pwsle  17547  pwsvscafval  17549  pwspjmhm  18890  pwsco1mhm  18892  pwsinvg  19120  mulgnngsum  19146  mulg1  19148  mulgnnp1  19149  mulgnnsubcl  19153  mulgnn0z  19168  mulgnndir  19170  mulgnn0di  19896  gsumconst  20005  pwslmod  21072  frlmvscaval  21899  psrlidm  22092  psrascl  22109  evlsscaval  22258  coe1tm  22415  coe1fzgsumd  22445  evl1scad  22476  evls1scafv  22507  decpmatid  22908  pmatcollpwscmatlem1  22927  lmconst  23399  cnconst2  23421  xkoptsub  23792  xkopt  23793  xkopjcn  23794  tmdgsum  24233  tmdgsum2  24234  symgtgp  24244  cstucnd  24421  pcoptcl  25161  pcopt  25162  pcopt2  25163  dvidlem  26055  dvconst  26057  dvnff  26063  dvn0  26064  dvcmul  26084  dvcmulf  26085  fta1blem  26309  plyeq0lem  26348  coemulc  26393  dgreq0  26403  dgrmulc  26409  qaa  26465  dchrisumlema  27630  exps1  28599  expsp1  28600  constcof  32944  suppovss  33004  fdifsuppconst  33012  evlscaval  33908  ofcc  34474  ofcof  34475  sseqf  34760  sseqp1  34763  lpadleft  35051  cvmlift3lem9  35797  ismrer1  38467  frlmvscadiccat  43258  fsuppssind  43305  ofoafo  44063  ofoaid1  44065  ofoaid2  44066  naddcnffo  44071  naddcnfid1  44074  dvsinax  46607  stoweidlem21  46715  stoweidlem47  46741  elaa2  46928  zlmodzxzscm  49114  2sphere0  49507  fvconstr  49617  fvconstrn0  49618