![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fconst6g | Structured version Visualization version Unicode version |
Description: Constant function with loose range. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Ref | Expression |
---|---|
fconst6g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconstg 5768 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | snssi 4115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | fssd 5736 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pr 4638 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-ral 2741 df-rex 2742 df-rab 2745 df-v 3046 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-sn 3968 df-pr 3970 df-op 3974 df-br 4402 df-opab 4461 df-mpt 4462 df-id 4748 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-fun 5583 df-fn 5584 df-f 5585 |
This theorem is referenced by: fconst6 5771 map0g 7508 fdiagfn 7512 mapsncnv 7515 brwdom2 8085 cantnf0 8177 fseqdom 8454 pwsdiagel 15388 setcmon 15975 setcepi 15976 pwsmnd 16564 pws0g 16565 0mhm 16598 pwspjmhm 16608 pwsgrp 16790 pwsinvg 16791 pwscmn 17494 pwsabl 17495 pwsring 17836 pws1 17837 pwscrng 17838 pwslmod 18186 psrvscacl 18610 psr0cl 18611 psrlmod 18618 mplsubglem 18651 coe1fval3 18794 coe1z 18849 coe1mul2 18855 coe1tm 18859 evls1sca 18905 frlmlmod 19305 frlmlss 19307 mamuvs1 19423 mamuvs2 19424 lmconst 20270 cnconst2 20292 pwstps 20638 xkopt 20663 xkopjcn 20664 tmdgsum 21103 tmdgsum2 21104 symgtgp 21109 cstucnd 21292 imasdsf1olem 21381 pwsxms 21540 pwsms 21541 mbfconstlem 22578 mbfmulc2lem 22596 i1fmulc 22654 itg2mulc 22698 dvconst 22864 dvcmul 22891 plypf1 23159 amgmlem 23908 dchrelbas2 24158 resf1o 28308 ofcccat 29423 poimirlem28 31961 lflvscl 32637 lflvsdi1 32638 lflvsdi2 32639 lflvsass 32641 constmap 35549 mendlmod 36053 dvsconst 36673 expgrowth 36678 dvsinax 37777 |
Copyright terms: Public domain | W3C validator |