Theorem fvconst2g 7231

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {csn 4588   × cxp 5653  ⟶wf 6554  ‘cfv 6558

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566

This theorem is used by:  fconst2g  7232  fvconst2  7233  ofc1  7745  ofc2  7746  caofid0l  7750  caofid0r  7751  caofid1  7752  caofid2  7753  fnsuppres  8236  ser0  14224  ser1const  14228  exp1  14237  expp1  14238  climconst2  15744  climaddc1  15831  climmulc2  15833  climsubc1  15834  climsubc2  15835  climlec2  15855  fsumconst  15985  supcvg  16054  prodf1  16089  prod0  16139  fprodconst  16174  seq1st  16775  algr0  16776  algrf  16777  ramz  17232  pwsbas  17687  pwsplusgval  17691  pwsmulrval  17692  pwsle  17693  pwsvscafval  17695  pwspjmhm  19055  pwsco1mhm  19057  pwsinvg  19292  mulgnngsum  19318  mulg1  19320  mulgnnp1  19321  mulgnnsubcl  19325  mulgnn0z  19340  mulgnndir  19342  mulgnn0di  20069  gsumconst  20178  pwslmod  21275  frlmvscaval  22104  psrlidm  22299  psrascl  22316  evlsscaval  22465  coe1tm  22622  coe1fzgsumd  22652  evl1scad  22683  evls1scafv  22714  decpmatid  23118  pmatcollpwscmatlem1  23137  lmconst  23609  cnconst2  23631  xkoptsub  24003  xkopt  24004  xkopjcn  24005  tmdgsum  24444  tmdgsum2  24445  symgtgp  24455  cstucnd  24632  pcoptcl  25372  pcopt  25373  pcopt2  25374  dvidlem  26265  dvconst  26267  dvnff  26273  dvn0  26274  dvcmul  26294  dvcmulf  26295  fta1blem  26519  plyeq0lem  26559  coemulc  26604  dgreq0  26614  dgrmulc  26620  qaa  26677  dchrisumlema  27845  exps1  28844  expsp1  28845  constcof  33287  suppovss  33345  fdifsuppconst  33353  evlscaval  34242  ofcc  34808  ofcof  34809  sseqf  35094  sseqp1  35097  lpadleft  35385  cvmlift3lem9  36259  ismrer1  38964  frlmvscadiccat  43766  fsuppssind  43814  ofoafo  44550  ofoaid1  44552  ofoaid2  44553  naddcnffo  44558  naddcnfid1  44561  dvsinax  47128  stoweidlem21  47236  stoweidlem47  47262  elaa2  47449  sqrtnnaa  48118  sqrtnzqaa  48119  zlmodzxzscm  49674  ovconstbrd  50178  ovconstbrn0d  50179