| 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 6795 | . 2 ⊢ (𝐵 ∈ 𝐷 → (𝐴 × {𝐵}):𝐴⟶{𝐵}) | |
| 2 | fvconst 7184 | . 2 ⊢ (((𝐴 × {𝐵}):𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | |
| 3 | 1, 2 | sylan 580 | 1 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 {csn 4626 × cxp 5683 ⟶wf 6557 ‘cfv 6561 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-fv 6569 |
| This theorem is referenced by: fconst2g 7223 fvconst2 7224 ofc1 7725 ofc2 7726 caofid0l 7730 caofid0r 7731 caofid1 7732 caofid2 7733 fnsuppres 8216 ser0 14095 ser1const 14099 exp1 14108 expp1 14109 climconst2 15584 climaddc1 15671 climmulc2 15673 climsubc1 15674 climsubc2 15675 climlec2 15695 fsumconst 15826 supcvg 15892 prodf1 15927 prod0 15979 fprodconst 16014 seq1st 16608 algr0 16609 algrf 16610 ramz 17063 pwsbas 17532 pwsplusgval 17535 pwsmulrval 17536 pwsle 17537 pwsvscafval 17539 pwspjmhm 18843 pwsco1mhm 18845 pwsinvg 19071 mulgnngsum 19097 mulg1 19099 mulgnnp1 19100 mulgnnsubcl 19104 mulgnn0z 19119 mulgnndir 19121 mulgnn0di 19843 gsumconst 19952 pwslmod 20968 frlmvscaval 21788 psrlidm 21982 psrascl 21999 coe1tm 22276 coe1fzgsumd 22308 evl1scad 22339 evls1scafv 22370 decpmatid 22776 pmatcollpwscmatlem1 22795 lmconst 23269 cnconst2 23291 xkoptsub 23662 xkopt 23663 xkopjcn 23664 tmdgsum 24103 tmdgsum2 24104 symgtgp 24114 cstucnd 24293 pcoptcl 25054 pcopt 25055 pcopt2 25056 dvidlem 25950 dvconst 25952 dvnff 25959 dvn0 25960 dvcmul 25981 dvcmulf 25982 fta1blem 26210 plyeq0lem 26249 coemulc 26294 dgreq0 26305 dgrmulc 26311 qaa 26365 dchrisumlema 27532 exps1 28411 expsp1 28412 suppovss 32690 fdifsuppconst 32698 ofcc 34107 ofcof 34108 sseqf 34394 sseqp1 34397 lpadleft 34698 cvmlift3lem9 35332 ismrer1 37845 frlmvscadiccat 42516 evlsscaval 42574 fsuppssind 42603 ofoafo 43369 ofoaid1 43371 ofoaid2 43372 naddcnffo 43377 naddcnfid1 43380 dvsinax 45928 stoweidlem21 46036 stoweidlem47 46062 elaa2 46249 zlmodzxzscm 48273 2sphere0 48671 fvconstr 48765 fvconstrn0 48766 |
| Copyright terms: Public domain | W3C validator |