![]() |
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.) Use its index-independent form baseid 17190 instead. (New usage is discouraged.) |
Ref | Expression |
---|---|
df-base | ⊢ Base = Slot 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbs 17187 | . 2 class Base | |
2 | c1 11147 | . . 3 class 1 | |
3 | 2 | cslot 17157 | . 2 class Slot 1 |
4 | 1, 3 | wceq 1533 | 1 wff Base = Slot 1 |
Colors of variables: wff setvar class |
This definition is referenced by: baseval 17189 baseid 17190 basendx 17196 basendxnnOLD 17198 1strwunOLD 17208 ressval3dOLD 17235 wunressOLD 17239 basendxnplusgndxOLD 17271 basendxnmulrndxOLD 17284 slotsbhcdifOLD 17404 wunfuncOLD 17895 wunnatOLD 17954 catcoppcclOLD 18114 catcfucclOLD 18116 estrreslem1OLD 18135 catcxpcclOLD 18206 oppgbasOLD 19311 symgvalstructOLD 19359 mgpbasOLD 20088 opprbasOLD 20288 rmodislmodOLD 20821 srabaseOLD 21071 zlmbasOLD 21452 znbas2OLD 21478 opsrbasOLD 21997 tngbasOLD 24572 ttgbasOLD 28704 baseltedgfOLD 28827 resvbasOLD 33069 hlhilsbaseOLD 41446 mnringbasedOLD 43680 |
Copyright terms: Public domain | W3C validator |