Metamath Proof Explorer
Table of Contents - 7.1.2. Slot definitions
- cplusg
- cmulr
- cstv
- csca
- cvsca
- cip
- cts
- cple
- coc
- cds
- cunif
- chom
- cco
- df-plusg
- df-mulr
- df-starv
- df-sca
- df-vsca
- df-ip
- df-tset
- df-ple
- df-ocomp
- df-ds
- df-unif
- df-hom
- df-cco
- plusgndx
- plusgid
- plusgndxnn
- basendxltplusgndx
- basendxnplusgndx
- basendxnplusgndxOLD
- grpstr
- grpstrndx
- grpbase
- grpbaseOLD
- grpplusg
- grpplusgOLD
- ressplusg
- grpbasex
- grpplusgx
- mulrndx
- mulrid
- basendxnmulrndx
- basendxnmulrndxOLD
- plusgndxnmulrndx
- rngstr
- rngbase
- rngplusg
- rngmulr
- starvndx
- starvid
- starvndxnbasendx
- starvndxnplusgndx
- starvndxnmulrndx
- ressmulr
- ressstarv
- srngstr
- srngbase
- srngplusg
- srngmulr
- srnginvl
- scandx
- scaid
- scandxnbasendx
- scandxnplusgndx
- scandxnmulrndx
- vscandx
- vscaid
- vscandxnbasendx
- vscandxnplusgndx
- vscandxnmulrndx
- vscandxnscandx
- lmodstr
- lmodbase
- lmodplusg
- lmodsca
- lmodvsca
- ipndx
- ipid
- ipndxnbasendx
- ipndxnplusgndx
- ipndxnmulrndx
- slotsdifipndx
- ipsstr
- ipsbase
- ipsaddg
- ipsmulr
- ipssca
- ipsvsca
- ipsip
- resssca
- ressvsca
- ressip
- phlstr
- phlbase
- phlplusg
- phlsca
- phlvsca
- phlip
- tsetndx
- tsetid
- tsetndxnn
- basendxlttsetndx
- tsetndxnbasendx
- tsetndxnplusgndx
- tsetndxnmulrndx
- tsetndxnstarvndx
- slotstnscsi
- topgrpstr
- topgrpbas
- topgrpplusg
- topgrptset
- resstset
- plendx
- pleid
- plendxnn
- basendxltplendx
- plendxnbasendx
- plendxnplusgndx
- plendxnmulrndx
- plendxnscandx
- plendxnvscandx
- slotsdifplendx
- otpsstr
- otpsbas
- otpstset
- otpsle
- ressle
- ocndx
- ocid
- basendxnocndx
- plendxnocndx
- dsndx
- dsid
- dsndxnn
- basendxltdsndx
- dsndxnbasendx
- dsndxnplusgndx
- dsndxnmulrndx
- slotsdnscsi
- dsndxntsetndx
- slotsdifdsndx
- unifndx
- unifid
- unifndxnn
- basendxltunifndx
- unifndxnbasendx
- unifndxntsetndx
- slotsdifunifndx
- ressunif
- odrngstr
- odrngbas
- odrngplusg
- odrngmulr
- odrngtset
- odrngle
- odrngds
- ressds
- homndx
- homid
- ccondx
- ccoid
- slotsbhcdif
- slotsbhcdifOLD
- slotsdifplendx2
- slotsdifocndx
- resshom
- ressco