![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > base0 | Structured version Visualization version Unicode version |
Description: The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Ref | Expression |
---|---|
base0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-base 15174 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | str0 15209 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-8 1899 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pow 4594 ax-pr 4652 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-rab 2757 df-v 3058 df-sbc 3279 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-uni 4212 df-br 4416 df-opab 4475 df-mpt 4476 df-id 4767 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-iota 5564 df-fun 5602 df-fv 5608 df-slot 15173 df-base 15174 |
This theorem is referenced by: elbasfv 15218 elbasov 15219 ressbasss 15229 ress0 15231 0cat 15642 oppcbas 15671 fucbas 15913 xpcbas 16111 xpchomfval 16112 xpccofval 16115 0pos 16248 meet0 16431 join0 16432 oduclatb 16438 isipodrs 16455 0g0 16554 frmdplusg 16686 grpn0 16746 grpinvfvi 16755 mulgfvi 16810 symgbas 17069 symgplusg 17078 psgnfval 17189 subcmn 17525 invrfval 17949 scaffval 18157 00lss 18213 00lsp 18252 asclfval 18606 psrbas 18650 psrplusg 18653 psrmulr 18656 resspsrbas 18687 opsrle 18747 00ply1bas 18881 ply1basfvi 18882 ply1plusgfvi 18883 thlbas 19307 dsmmbas2 19348 dsmmfi 19349 matbas0pc 19482 matbas0 19483 matrcl 19485 mdetfval 19659 madufval 19710 mdegfval 23059 uc1pval 23138 mon1pval 23140 dchrrcl 24216 submomnd 28521 suborng 28626 mendbas 36094 mendplusgfval 36095 mendmulrfval 36097 mendvscafval 36100 vtxval0 39184 |
Copyright terms: Public domain | W3C validator |