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

Definition df-base 13505
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 13500 . 2  class  Base
2 c1 9022 . . 3  class  1
32cslot 13499 . 2  class Slot  1
41, 3wceq 1653 1  wff  Base  = Slot  1
Colors of variables: wff set class
This definition is referenced by:  base0  13537  baseval  13541  baseid  13542  basendx  13545  wunress  13559  wunfunc  14127  wunnat  14184  catcoppccl  14294  catcfuccl  14295  catcxpccl  14335  oppgbas  15178  mgpbas  15685  opprbas  15765  srabase  16281  rlmscaf  16310  opsrbas  16570  ply1tmcl  16695  ply1scltm  16704  ply1sclf  16708  ply1scl0  16712  ply1scl1  16714  zlmbas  16830  znbas2  16851  tngbas  18713  nrgtrg  18756  basfn  27280  hlhilsbase  32838
  Copyright terms: Public domain W3C validator