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 or carrier set) extractor for posets and related 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 15695 | . 2 class Base | |
2 | c1 9816 | . . 3 class 1 | |
3 | 2 | cslot 15694 | . 2 class Slot 1 |
4 | 1, 3 | wceq 1475 | 1 wff Base = Slot 1 |
Colors of variables: wff setvar class |
This definition is referenced by: base0 15740 baseval 15746 baseid 15747 basendx 15751 basendxnn 15752 ressval3d 15764 wunress 15767 1strwun 15808 slotsbhcdif 15903 wunfunc 16382 wunnat 16439 catcoppccl 16581 catcfuccl 16582 bascnvimaeqv 16584 estrcbasbas 16594 estrreslem1 16600 catcxpccl 16670 oppgbas 17604 mgpbas 18318 opprbas 18452 srabase 18999 rlmscaf 19029 opsrbas 19300 ply1tmcl 19463 ply1scltm 19472 ply1sclf 19476 ply1scl0 19481 ply1scl1 19483 zlmbas 19685 znbas2 19707 tngbas 22255 nrgtrg 22304 ttgbas 25557 baseltedgf 25671 basvtxval 25693 resvbas 29163 hlhilsbase 36249 basfn 36689 basendxnmulrndx 41744 ringcbasbas 41826 ringcbasbasALTV 41850 |
Copyright terms: Public domain | W3C validator |