![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > base0 | Structured version Visualization version GIF version |
Description: The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Ref | Expression |
---|---|
base0 | ⊢ ∅ = (Base‘∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-base 16187 | . 2 ⊢ Base = Slot 1 | |
2 | 1 | str0 16233 | 1 ⊢ ∅ = (Base‘∅) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1653 ∅c0 4113 ‘cfv 6099 1c1 10223 Basecbs 16181 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-sep 4973 ax-nul 4981 ax-pow 5033 ax-pr 5095 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ral 3092 df-rex 3093 df-rab 3096 df-v 3385 df-sbc 3632 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-nul 4114 df-if 4276 df-sn 4367 df-pr 4369 df-op 4373 df-uni 4627 df-br 4842 df-opab 4904 df-mpt 4921 df-id 5218 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-iota 6062 df-fun 6101 df-fv 6107 df-slot 16185 df-base 16187 |
This theorem is referenced by: elbasfv 16242 elbasov 16243 ressbasss 16254 ress0 16256 0cat 16660 oppcbas 16689 fucbas 16931 xpcbas 17130 xpchomfval 17131 xpccofval 17134 0pos 17266 meet0 17449 join0 17450 oduclatb 17456 isipodrs 17473 0g0 17575 frmdplusg 17704 grpn0 17767 grpinvfvi 17776 mulgfvi 17858 symgbas 18109 symgplusg 18118 psgnfval 18230 subcmn 18554 invrfval 18986 scaffval 19196 00lss 19257 00lsp 19299 asclfval 19654 psrbas 19698 psrplusg 19701 psrmulr 19704 resspsrbas 19735 opsrle 19795 00ply1bas 19929 ply1basfvi 19930 ply1plusgfvi 19931 thlbas 20362 dsmmbas2 20403 dsmmfi 20404 matbas0pc 20537 matbas0 20538 matrcl 20540 mdetfval 20715 madufval 20766 mdegfval 24160 uc1pval 24237 mon1pval 24239 dchrrcl 25314 vtxval0 26266 submomnd 30218 suborng 30323 mendbas 38527 mendplusgfval 38528 mendmulrfval 38530 mendvscafval 38533 |
Copyright terms: Public domain | W3C validator |