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 15857
Description: Define the base set (also called underlying set or carrier set) extractor for extensible 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 15851 . 2 class Base
2 c1 9934 . . 3 class 1
32cslot 15850 . 2 class Slot 1
41, 3wceq 1482 1 wff Base = Slot 1
Colors of variables: wff setvar class
This definition is referenced by:  basfn  15871  base0  15906  baseval  15912  baseid  15913  basendx  15917  basendxnn  15918  ressval3d  15931  wunress  15934  1strwun  15976  basendxnplusgndx  15983  basendxnmulrndx  15993  slotsbhcdif  16074  wunfunc  16553  wunnat  16610  catcoppccl  16752  catcfuccl  16753  bascnvimaeqv  16755  estrcbasbas  16765  estrreslem1  16771  catcxpccl  16841  oppgbas  17775  mgpbas  18489  opprbas  18623  rmodislmod  18925  srabase  19172  rlmscaf  19202  opsrbas  19473  ply1tmcl  19636  ply1scltm  19645  ply1sclf  19649  ply1scl0  19654  ply1scl1  19656  zlmbas  19860  znbas2  19882  tngbas  22439  nrgtrg  22488  ttgbas  25751  baseltedgf  25866  basvtxvalOLD  25897  resvbas  29817  hlhilsbase  37057  ringcbasbas  41805  ringcbasbasALTV  41829
  Copyright terms: Public domain W3C validator