Theorem fvconst2g 7204

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  {csn 4606   × cxp 5663  ⟶wf 6537  ‘cfv 6541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549

This theorem is referenced by:  fconst2g  7205  fvconst2  7206  ofc1  7707  ofc2  7708  caofid0l  7712  caofid0r  7713  caofid1  7714  caofid2  7715  fnsuppres  8198  ser0  14077  ser1const  14081  exp1  14090  expp1  14091  climconst2  15566  climaddc1  15653  climmulc2  15655  climsubc1  15656  climsubc2  15657  climlec2  15677  fsumconst  15808  supcvg  15874  prodf1  15909  prod0  15961  fprodconst  15996  seq1st  16590  algr0  16591  algrf  16592  ramz  17045  pwsbas  17503  pwsplusgval  17506  pwsmulrval  17507  pwsle  17508  pwsvscafval  17510  pwspjmhm  18812  pwsco1mhm  18814  pwsinvg  19040  mulgnngsum  19066  mulg1  19068  mulgnnp1  19069  mulgnnsubcl  19073  mulgnn0z  19088  mulgnndir  19090  mulgnn0di  19811  gsumconst  19920  pwslmod  20936  frlmvscaval  21742  psrlidm  21936  psrascl  21953  coe1tm  22224  coe1fzgsumd  22256  evl1scad  22287  evls1scafv  22318  decpmatid  22724  pmatcollpwscmatlem1  22743  lmconst  23215  cnconst2  23237  xkoptsub  23608  xkopt  23609  xkopjcn  23610  tmdgsum  24049  tmdgsum2  24050  symgtgp  24060  cstucnd  24238  pcoptcl  24990  pcopt  24991  pcopt2  24992  dvidlem  25886  dvconst  25888  dvnff  25895  dvn0  25896  dvcmul  25917  dvcmulf  25918  fta1blem  26146  plyeq0lem  26185  coemulc  26230  dgreq0  26241  dgrmulc  26247  qaa  26301  dchrisumlema  27468  exps1  28347  expsp1  28348  suppovss  32625  fdifsuppconst  32633  ofcc  34066  ofcof  34067  sseqf  34353  sseqp1  34356  lpadleft  34657  cvmlift3lem9  35291  ismrer1  37804  frlmvscadiccat  42479  evlsscaval  42537  fsuppssind  42566  ofoafo  43331  ofoaid1  43333  ofoaid2  43334  naddcnffo  43339  naddcnfid1  43342  dvsinax  45885  stoweidlem21  45993  stoweidlem47  46019  elaa2  46206  zlmodzxzscm  48231  2sphere0  48629  fvconstr  48723  fvconstrn0  48724