Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fconst6g | Structured version Visualization version GIF version |
Description: Constant function with loose range. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Ref | Expression |
---|---|
fconst6g | ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconstg 6559 | . 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶{𝐵}) | |
2 | snssi 4733 | . 2 ⊢ (𝐵 ∈ 𝐶 → {𝐵} ⊆ 𝐶) | |
3 | 1, 2 | fssd 6521 | 1 ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 {csn 4557 × cxp 5546 ⟶wf 6344 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-ral 3140 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-fun 6350 df-fn 6351 df-f 6352 |
This theorem is referenced by: fconst6 6562 map0g 8437 fdiagfn 8442 mapsncnv 8445 brwdom2 9025 cantnf0 9126 fseqdom 9440 pwsdiagel 16758 setcmon 17335 setcepi 17336 pwsmnd 17934 pws0g 17935 0mhm 17972 pwspjmhm 17982 pwsgrp 18149 pwsinvg 18150 pwscmn 18912 pwsabl 18913 pwsring 19294 pws1 19295 pwscrng 19296 pwslmod 19671 psrvscacl 20101 psr0cl 20102 psrlmod 20109 mplsubglem 20142 coe1fval3 20304 coe1z 20359 coe1mul2 20365 coe1tm 20369 evls1sca 20414 frlmlmod 20821 frlmlss 20823 mamuvs1 20942 mamuvs2 20943 lmconst 21797 cnconst2 21819 pwstps 22166 xkopt 22191 xkopjcn 22192 tmdgsum 22631 tmdgsum2 22632 symgtgp 22637 cstucnd 22820 imasdsf1olem 22910 pwsxms 23069 pwsms 23070 mbfconstlem 24155 mbfmulc2lem 24175 i1fmulc 24231 itg2mulc 24275 dvconst 24441 dvcmul 24468 plypf1 24729 amgmlem 25494 dchrelbas2 25740 resf1o 30392 ofcccat 31712 lpadlem1 31847 poimirlem28 34801 lflvscl 36093 lflvsdi1 36094 lflvsdi2 36095 lflvsass 36097 constmap 39188 mendlmod 39671 dvsconst 40539 expgrowth 40544 mapssbi 41352 dvsinax 42073 amgmlemALT 44832 |
Copyright terms: Public domain | W3C validator |