![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvconst2g | Structured version Visualization version GIF version |
Description: The value of a constant function. (Contributed by NM, 20-Aug-2005.) |
Ref | Expression |
---|---|
fvconst2g | ⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconstg 6540 | . 2 ⊢ (𝐵 ∈ 𝐷 → (𝐴 × {𝐵}):𝐴⟶{𝐵}) | |
2 | fvconst 6903 | . 2 ⊢ (((𝐴 × {𝐵}):𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | |
3 | 1, 2 | sylan 583 | 1 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 {csn 4525 × cxp 5517 ⟶wf 6320 ‘cfv 6324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-fv 6332 |
This theorem is referenced by: fconst2g 6942 fvconst2 6943 ofc1 7412 ofc2 7413 caofid0l 7417 caofid0r 7418 caofid1 7419 caofid2 7420 fnsuppres 7840 ser0 13418 ser1const 13422 exp1 13431 expp1 13432 climconst2 14897 climaddc1 14983 climmulc2 14985 climsubc1 14986 climsubc2 14987 climlec2 15007 fsumconst 15137 supcvg 15203 prodf1 15239 prod0 15289 fprodconst 15324 seq1st 15905 algr0 15906 algrf 15907 ramz 16351 pwsbas 16752 pwsplusgval 16755 pwsmulrval 16756 pwsle 16757 pwsvscafval 16759 pwspjmhm 17986 pwsco1mhm 17988 pwsinvg 18204 mulgnngsum 18225 mulg1 18227 mulgnnp1 18228 mulgnnsubcl 18232 mulgnn0z 18246 mulgnndir 18248 mulgnn0di 18939 gsumconst 19047 pwslmod 19735 frlmvscaval 20457 psrlidm 20641 coe1tm 20902 coe1fzgsumd 20931 evl1scad 20959 decpmatid 21375 pmatcollpwscmatlem1 21394 lmconst 21866 cnconst2 21888 xkoptsub 22259 xkopt 22260 xkopjcn 22261 tmdgsum 22700 tmdgsum2 22701 symgtgp 22711 cstucnd 22890 pcoptcl 23626 pcopt 23627 pcopt2 23628 dvidlem 24518 dvconst 24520 dvnff 24526 dvn0 24527 dvcmul 24547 dvcmulf 24548 fta1blem 24769 plyeq0lem 24807 coemulc 24852 dgreq0 24862 dgrmulc 24868 qaa 24919 dchrisumlema 26072 suppovss 30443 fdifsuppconst 30449 ofcc 31475 ofcof 31476 sseqf 31760 sseqp1 31763 lpadleft 32064 cvmlift3lem9 32687 ismrer1 35276 frlmvscadiccat 39440 fsuppssind 39459 dvsinax 42555 stoweidlem21 42663 stoweidlem47 42689 elaa2 42876 zlmodzxzscm 44759 2sphere0 45164 |
Copyright terms: Public domain | W3C validator |