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

Definition df-base 13153
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 13148 . 2  class  Base
2 c1 8738 . . 3  class  1
32cslot 13147 . 2  class Slot  1
41, 3wceq 1623 1  wff  Base  = Slot  1
Colors of variables: wff set class
This definition is referenced by:  base0  13185  baseval  13189  baseid  13190  basendx  13193  wunress  13207  oppcbas  13621  wunfunc  13773  wunnat  13830  catcoppccl  13940  catcfuccl  13941  catcxpccl  13981  oppgbas  14824  mgpbas  15331  opprbas  15411  srabase  15931  rlmscaf  15960  opsrbas  16220  ply1tmcl  16348  ply1scltm  16357  ply1sclf  16361  ply1scl0  16365  ply1scl1  16367  zlmbas  16472  znbas2  16493  tngbas  18157  nrgtrg  18200  basfn  27265  hlhilsbase  32132
  Copyright terms: Public domain W3C validator