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

Definition df-base 13148
Description: Define the base 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 13143 . 2  class  Base
2 c1 8734 . . 3  class  1
32cslot 13142 . 2  class Slot  1
41, 3wceq 1624 1  wff  Base  = Slot  1
Colors of variables: wff set class
This definition is referenced by:  base0  13180  baseval  13184  baseid  13185  basendx  13188  wunress  13202  oppcbas  13616  wunfunc  13768  wunnat  13825  catcoppccl  13935  catcfuccl  13936  catcxpccl  13976  oppgbas  14819  mgpbas  15326  opprbas  15406  srabase  15926  rlmscaf  15955  opsrbas  16215  ply1tmcl  16343  ply1scltm  16352  ply1sclf  16356  ply1scl0  16360  ply1scl1  16362  zlmbas  16467  znbas2  16488  tngbas  18152  nrgtrg  18195  basfn  26665  hlhilsbase  31400
  Copyright terms: Public domain W3C validator