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 15700
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 15695 . 2 class Base
2 c1 9816 . . 3 class 1
32cslot 15694 . 2 class Slot 1
41, 3wceq 1475 1 wff Base = Slot 1
Colors of variables: wff setvar class
This definition is referenced by:  base0  15740  baseval  15746  baseid  15747  basendx  15751  basendxnn  15752  ressval3d  15764  wunress  15767  1strwun  15808  slotsbhcdif  15903  wunfunc  16382  wunnat  16439  catcoppccl  16581  catcfuccl  16582  bascnvimaeqv  16584  estrcbasbas  16594  estrreslem1  16600  catcxpccl  16670  oppgbas  17604  mgpbas  18318  opprbas  18452  srabase  18999  rlmscaf  19029  opsrbas  19300  ply1tmcl  19463  ply1scltm  19472  ply1sclf  19476  ply1scl0  19481  ply1scl1  19483  zlmbas  19685  znbas2  19707  tngbas  22255  nrgtrg  22304  ttgbas  25557  baseltedgf  25671  basvtxval  25693  resvbas  29163  hlhilsbase  36249  basfn  36689  basendxnmulrndx  41744  ringcbasbas  41826  ringcbasbasALTV  41850
  Copyright terms: Public domain W3C validator