| 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 17250 instead. (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| df-base | ⊢ Base = Slot 1 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbs 17247 | . 2 class Base | |
| 2 | c1 11156 | . . 3 class 1 | |
| 3 | 2 | cslot 17218 | . 2 class Slot 1 |
| 4 | 1, 3 | wceq 1540 | 1 wff Base = Slot 1 |
| Colors of variables: wff setvar class |
| This definition is referenced by: baseval 17249 baseid 17250 basendx 17256 wunressOLD 17296 basendxnmulrndxOLD 17340 slotsbhcdifOLD 17460 estrreslem1OLD 18182 symgvalstructOLD 19415 opprbasOLD 20342 srabaseOLD 21178 zlmbasOLD 21530 znbas2OLD 21556 opsrbasOLD 22070 tngbasOLD 24656 ttgbasOLD 28888 baseltedgfOLD 29011 resvbasOLD 33360 hlhilsbaseOLD 41943 sn-base0 42505 mnringbasedOLD 44231 |
| Copyright terms: Public domain | W3C validator |