Theorem fvconst2g 7200

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {csn 4584   × cxp 5649  ⟶wf 6527  ‘cfv 6531

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539

This theorem is used by:  fconst2g  7201  fvconst2  7202  ofc1  7710  ofc2  7711  caofid0l  7715  caofid0r  7716  caofid1  7717  caofid2  7718  fnsuppres  8192  ser0  14177  ser1const  14181  exp1  14190  expp1  14191  climconst2  15695  climaddc1  15782  climmulc2  15784  climsubc1  15785  climsubc2  15786  climlec2  15806  fsumconst  15936  supcvg  16005  prodf1  16040  prod0  16090  fprodconst  16125  seq1st  16726  algr0  16727  algrf  16728  ramz  17183  pwsbas  17638  pwsplusgval  17642  pwsmulrval  17643  pwsle  17644  pwsvscafval  17646  pwspjmhm  19006  pwsco1mhm  19008  pwsinvg  19243  mulgnngsum  19269  mulg1  19271  mulgnnp1  19272  mulgnnsubcl  19276  mulgnn0z  19291  mulgnndir  19293  mulgnn0di  20019  gsumconst  20128  pwslmod  21225  frlmvscaval  22054  psrlidm  22249  psrascl  22266  evlsscaval  22415  coe1tm  22572  coe1fzgsumd  22602  evl1scad  22633  evls1scafv  22664  decpmatid  23068  pmatcollpwscmatlem1  23087  lmconst  23559  cnconst2  23581  xkoptsub  23953  xkopt  23954  xkopjcn  23955  tmdgsum  24394  tmdgsum2  24395  symgtgp  24405  cstucnd  24582  pcoptcl  25322  pcopt  25323  pcopt2  25324  dvidlem  26215  dvconst  26217  dvnff  26223  dvn0  26224  dvcmul  26244  dvcmulf  26245  fta1blem  26469  plyeq0lem  26509  coemulc  26554  dgreq0  26564  dgrmulc  26570  qaa  26629  dchrisumlema  27797  exps1  28796  expsp1  28797  constcof  33197  suppovss  33256  fdifsuppconst  33264  evlscaval  34154  ofcc  34720  ofcof  34721  sseqf  35007  sseqp1  35010  lpadleft  35298  cvmlift3lem9  36061  ismrer1  38740  frlmvscadiccat  43538  fsuppssind  43583  ofoafo  44316  ofoaid1  44318  ofoaid2  44319  naddcnffo  44324  naddcnfid1  44327  dvsinax  46867  stoweidlem21  46975  stoweidlem47  47001  elaa2  47188  sqrtnnaa  47857  sqrtnzqaa  47858  zlmodzxzscm  49413  2sphere0  49806  ovconstbrd  49916  ovconstbrn0d  49917