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 16473 | . 2 class Base | |
2 | c1 10527 | . . 3 class 1 | |
3 | 2 | cslot 16472 | . 2 class Slot 1 |
4 | 1, 3 | wceq 1528 | 1 wff Base = Slot 1 |
Colors of variables: wff setvar class |
This definition is referenced by: basfn 16493 base0 16526 baseval 16532 baseid 16533 basendx 16537 basendxnn 16538 ressval3d 16551 wunress 16554 1strwun 16591 basendxnplusgndx 16598 basendxnmulrndx 16608 slotsbhcdif 16683 wunfunc 17159 wunnat 17216 catcoppccl 17358 catcfuccl 17359 estrcbasbas 17371 estrreslem1 17377 catcxpccl 17447 oppgbas 18419 mgpbas 19176 opprbas 19310 rmodislmod 19633 srabase 19881 rlmscaf 19911 opsrbas 20189 ply1tmcl 20370 ply1scltm 20379 ply1sclf 20383 ply1scl0 20388 ply1scl1 20390 zlmbas 20595 znbas2 20616 tngbas 23179 nrgtrg 23228 ttgbas 26591 baseltedgf 26707 resvbas 30833 hlhilsbase 38957 ringcbasbas 44203 ringcbasbasALTV 44227 |
Copyright terms: Public domain | W3C validator |