MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-base Structured version   Visualization version   GIF version

Definition df-base 15642
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.)
Assertion
Ref Expression
df-base Base = Slot 1

Detailed syntax breakdown of Definition df-base
StepHypRef Expression
1 cbs 15637 . 2 class Base
2 c1 9789 . . 3 class 1
32cslot 15636 . 2 class Slot 1
41, 3wceq 1474 1 wff Base = Slot 1
Colors of variables: wff setvar class
This definition is referenced by:  base0  15682  baseval  15688  baseid  15689  basendx  15693  basendxnn  15694  ressval3d  15706  wunress  15709  1strwun  15750  slotsbhcdif  15845  wunfunc  16324  wunnat  16381  catcoppccl  16523  catcfuccl  16524  bascnvimaeqv  16526  estrcbasbas  16536  estrreslem1  16542  catcxpccl  16612  oppgbas  17546  mgpbas  18260  opprbas  18394  srabase  18941  rlmscaf  18971  opsrbas  19242  ply1tmcl  19405  ply1scltm  19414  ply1sclf  19418  ply1scl0  19423  ply1scl1  19425  zlmbas  19626  znbas2  19648  tngbas  22189  nrgtrg  22233  ttgbas  25471  resvbas  28965  hlhilsbase  36048  basfn  36488  baseltedgf  40225  basvtxval  40247  basendxnmulrndx  41742  ringcbasbas  41824  ringcbasbasALTV  41848
  Copyright terms: Public domain W3C validator