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

Definition df-base 13169
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 13164 . 2  class  Base
2 c1 8754 . . 3  class  1
32cslot 13163 . 2  class Slot  1
41, 3wceq 1632 1  wff  Base  = Slot  1
Colors of variables: wff set class
This definition is referenced by:  base0  13201  baseval  13205  baseid  13206  basendx  13209  wunress  13223  oppcbas  13637  wunfunc  13789  wunnat  13846  catcoppccl  13956  catcfuccl  13957  catcxpccl  13997  oppgbas  14840  mgpbas  15347  opprbas  15427  srabase  15947  rlmscaf  15976  opsrbas  16236  ply1tmcl  16364  ply1scltm  16373  ply1sclf  16377  ply1scl0  16381  ply1scl1  16383  zlmbas  16488  znbas2  16509  tngbas  18173  nrgtrg  18216  basfn  27368  hlhilsbase  32754
  Copyright terms: Public domain W3C validator