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

Definition df-base 15805
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 15800 . 2 class Base
2 c1 9897 . . 3 class 1
32cslot 15799 . 2 class Slot 1
41, 3wceq 1480 1 wff Base = Slot 1
Colors of variables: wff setvar class
This definition is referenced by:  base0  15852  baseval  15858  baseid  15859  basendx  15863  basendxnn  15864  ressval3d  15877  wunress  15880  1strwun  15922  basendxnplusgndx  15929  basendxnmulrndx  15939  slotsbhcdif  16020  wunfunc  16499  wunnat  16556  catcoppccl  16698  catcfuccl  16699  bascnvimaeqv  16701  estrcbasbas  16711  estrreslem1  16717  catcxpccl  16787  oppgbas  17721  mgpbas  18435  opprbas  18569  rmodislmod  18871  srabase  19118  rlmscaf  19148  opsrbas  19419  ply1tmcl  19582  ply1scltm  19591  ply1sclf  19595  ply1scl0  19600  ply1scl1  19602  zlmbas  19806  znbas2  19828  tngbas  22385  nrgtrg  22434  ttgbas  25691  baseltedgf  25806  basvtxvalOLD  25837  resvbas  29659  hlhilsbase  36750  basfn  37190  ringcbasbas  41352  ringcbasbasALTV  41376
  Copyright terms: Public domain W3C validator