![]() |
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 16481 | . 2 ⊢ Base = Slot 1 | |
2 | 1 | str0 16527 | 1 ⊢ ∅ = (Base‘∅) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1538 ∅c0 4243 ‘cfv 6324 1c1 10527 Basecbs 16475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-iota 6283 df-fun 6326 df-fv 6332 df-slot 16479 df-base 16481 |
This theorem is referenced by: elbasfv 16536 elbasov 16537 ressbasss 16548 ress0 16550 0cat 16951 oppcbas 16980 fucbas 17222 xpcbas 17420 xpchomfval 17421 xpccofval 17424 0pos 17556 meet0 17739 join0 17740 oduclatb 17746 isipodrs 17763 0g0 17866 frmdplusg 18011 efmndbas 18028 efmndbasabf 18029 efmndplusg 18037 grpn0 18127 grpinvfvi 18138 mulgfvi 18222 psgnfval 18620 subcmn 18950 invrfval 19419 00lss 19706 00lsp 19746 thlbas 20385 dsmmfi 20427 asclfval 20565 psrbas 20616 psrplusg 20619 psrmulr 20622 resspsrbas 20653 opsrle 20715 00ply1bas 20869 ply1basfvi 20870 ply1plusgfvi 20871 matbas0pc 21014 matbas0 21015 matrcl 21017 mdetfval 21191 madufval 21242 mdegfval 24663 uc1pval 24740 mon1pval 24742 dchrrcl 25824 vtxval0 26832 submomnd 30761 suborng 30939 bj-isrvec 34708 mendbas 40128 mendplusgfval 40129 mendmulrfval 40131 mendvscafval 40134 |
Copyright terms: Public domain | W3C validator |