Theorem fvconst2g 7207

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  {csn 4594   × cxp 5664  ⟶wf 6539  ‘cfv 6543

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551

This theorem is used by:  fconst2g  7208  fvconst2  7209  ofc1  7715  ofc2  7716  caofid0l  7720  caofid0r  7721  caofid1  7722  caofid2  7723  fnsuppres  8196  ser0  14110  ser1const  14114  exp1  14123  expp1  14124  climconst2  15625  climaddc1  15712  climmulc2  15714  climsubc1  15715  climsubc2  15716  climlec2  15736  fsumconst  15867  supcvg  15936  prodf1  15971  prod0  16023  fprodconst  16058  seq1st  16654  algr0  16655  algrf  16656  ramz  17110  pwsbas  17565  pwsplusgval  17569  pwsmulrval  17570  pwsle  17571  pwsvscafval  17573  pwspjmhm  18920  pwsco1mhm  18922  pwsinvg  19150  mulgnngsum  19176  mulg1  19178  mulgnnp1  19179  mulgnnsubcl  19183  mulgnn0z  19198  mulgnndir  19200  mulgnn0di  19926  gsumconst  20035  pwslmod  21128  frlmvscaval  21955  psrlidm  22148  psrascl  22165  evlsscaval  22314  coe1tm  22471  coe1fzgsumd  22501  evl1scad  22532  evls1scafv  22563  decpmatid  22964  pmatcollpwscmatlem1  22983  lmconst  23455  cnconst2  23477  xkoptsub  23848  xkopt  23849  xkopjcn  23850  tmdgsum  24289  tmdgsum2  24290  symgtgp  24300  cstucnd  24477  pcoptcl  25217  pcopt  25218  pcopt2  25219  dvidlem  26111  dvconst  26113  dvnff  26119  dvn0  26120  dvcmul  26140  dvcmulf  26141  fta1blem  26365  plyeq0lem  26404  coemulc  26449  dgreq0  26459  dgrmulc  26465  qaa  26521  dchrisumlema  27689  exps1  28658  expsp1  28659  constcof  33003  suppovss  33063  fdifsuppconst  33071  evlscaval  33961  ofcc  34527  ofcof  34528  sseqf  34814  sseqp1  34817  lpadleft  35105  cvmlift3lem9  35840  ismrer1  38530  frlmvscadiccat  43321  fsuppssind  43366  ofoafo  44124  ofoaid1  44126  ofoaid2  44127  naddcnffo  44132  naddcnfid1  44135  dvsinax  46668  stoweidlem21  46776  stoweidlem47  46802  elaa2  46989  sqrtnnaa  47645  sqrtnzqaa  47646  zlmodzxzscm  49178  2sphere0  49571  fvconstr  49681  fvconstrn0  49682