![]() |
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 16312 | . 2 class Base | |
2 | c1 10384 | . . 3 class 1 | |
3 | 2 | cslot 16311 | . 2 class Slot 1 |
4 | 1, 3 | wceq 1522 | 1 wff Base = Slot 1 |
Colors of variables: wff setvar class |
This definition is referenced by: basfn 16332 base0 16365 baseval 16371 baseid 16372 basendx 16376 basendxnn 16377 ressval3d 16390 wunress 16393 1strwun 16430 basendxnplusgndx 16437 basendxnmulrndx 16447 slotsbhcdif 16522 wunfunc 16998 wunnat 17055 catcoppccl 17197 catcfuccl 17198 estrcbasbas 17210 estrreslem1 17216 catcxpccl 17286 oppgbas 18220 mgpbas 18935 opprbas 19069 rmodislmod 19392 srabase 19640 rlmscaf 19670 opsrbas 19946 ply1tmcl 20123 ply1scltm 20132 ply1sclf 20136 ply1scl0 20141 ply1scl1 20143 zlmbas 20347 znbas2 20368 tngbas 22933 nrgtrg 22982 ttgbas 26346 baseltedgf 26462 resvbas 30559 hlhilsbase 38606 ringcbasbas 43783 ringcbasbasALTV 43807 |
Copyright terms: Public domain | W3C validator |