Definition df-base 15863

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

Step	Hyp	Ref	Expression
1		cbs 15857	. 2 class Base
2		c1 9937	. . 3 class 1
3	2	cslot 15856	. 2 class Slot 1
4	1, 3	wceq 1483	1 wff Base = Slot 1

This definition is referenced by:  basfn  15877  base0  15912  baseval  15918  baseid  15919  basendx  15923  basendxnn  15924  ressval3d  15937  wunress  15940  1strwun  15982  basendxnplusgndx  15989  basendxnmulrndx  15999  slotsbhcdif  16080  wunfunc  16559  wunnat  16616  catcoppccl  16758  catcfuccl  16759  bascnvimaeqv  16761  estrcbasbas  16771  estrreslem1  16777  catcxpccl  16847  oppgbas  17781  mgpbas  18495  opprbas  18629  rmodislmod  18931  srabase  19178  rlmscaf  19208  opsrbas  19479  ply1tmcl  19642  ply1scltm  19651  ply1sclf  19655  ply1scl0  19660  ply1scl1  19662  zlmbas  19866  znbas2  19888  tngbas  22445  nrgtrg  22494  ttgbas  25757  baseltedgf  25872  basvtxvalOLD  25903  resvbas  29832  hlhilsbase  37231  ringcbasbas  42034  ringcbasbasALTV  42058