![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-base | Structured version Visualization version GIF version |
Description: Define the base set (also called underlying set, ground set, carrier set, or carrier) extractor for extensible structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
Ref | Expression |
---|---|
df-base | ⊢ Base = Slot 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbs 16221 | . 2 class Base | |
2 | c1 10252 | . . 3 class 1 | |
3 | 2 | cslot 16220 | . 2 class Slot 1 |
4 | 1, 3 | wceq 1658 | 1 wff Base = Slot 1 |
Colors of variables: wff setvar class |
This definition is referenced by: basfn 16241 base0 16274 baseval 16280 baseid 16281 basendx 16285 basendxnn 16286 ressval3d 16299 ressval3dOLD 16300 wunress 16303 1strwun 16340 basendxnplusgndx 16347 basendxnmulrndx 16357 slotsbhcdif 16432 wunfunc 16910 wunnat 16967 catcoppccl 17109 catcfuccl 17110 bascnvimaeqv 17112 estrcbasbas 17122 estrreslem1 17128 catcxpccl 17199 oppgbas 18130 mgpbas 18848 opprbas 18982 rmodislmod 19286 srabase 19538 rlmscaf 19568 opsrbas 19838 ply1tmcl 20001 ply1scltm 20010 ply1sclf 20014 ply1scl0 20019 ply1scl1 20021 zlmbas 20225 znbas2 20246 tngbas 22814 nrgtrg 22863 ttgbas 26175 baseltedgf 26291 resvbas 30376 hlhilsbase 38013 ringcbasbas 42880 ringcbasbasALTV 42904 |
Copyright terms: Public domain | W3C validator |