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

Definition df-base 13457
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 13452 . 2  class  Base
2 c1 8975 . . 3  class  1
32cslot 13451 . 2  class Slot  1
41, 3wceq 1652 1  wff  Base  = Slot  1
Colors of variables: wff set class
This definition is referenced by:  base0  13489  baseval  13493  baseid  13494  basendx  13497  wunress  13511  wunfunc  14079  wunnat  14136  catcoppccl  14246  catcfuccl  14247  catcxpccl  14287  oppgbas  15130  mgpbas  15637  opprbas  15717  srabase  16233  rlmscaf  16262  opsrbas  16522  ply1tmcl  16647  ply1scltm  16656  ply1sclf  16660  ply1scl0  16664  ply1scl1  16666  zlmbas  16782  znbas2  16803  tngbas  18665  nrgtrg  18708  basfn  27175  hlhilsbase  32471
  Copyright terms: Public domain W3C validator