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

Definition df-base 13429
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 13424 . 2  class  Base
2 c1 8947 . . 3  class  1
32cslot 13423 . 2  class Slot  1
41, 3wceq 1649 1  wff  Base  = Slot  1
Colors of variables: wff set class
This definition is referenced by:  base0  13461  baseval  13465  baseid  13466  basendx  13469  wunress  13483  wunfunc  14051  wunnat  14108  catcoppccl  14218  catcfuccl  14219  catcxpccl  14259  oppgbas  15102  mgpbas  15609  opprbas  15689  srabase  16205  rlmscaf  16234  opsrbas  16494  ply1tmcl  16619  ply1scltm  16628  ply1sclf  16632  ply1scl0  16636  ply1scl1  16638  zlmbas  16754  znbas2  16775  tngbas  18635  nrgtrg  18678  basfn  27133  hlhilsbase  32425
  Copyright terms: Public domain W3C validator