wss - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > wss		Structured version Visualization version Unicode version

Syntax Definition wss 3574

Description: Extend wff notation to include the subclass relation. This is read "

is a subclass of

" or "

includes

." When

exists as a set, it is also read "

is a subset of

**Hypotheses**
Ref	Expression
cA
cB

**Assertion**
Ref	Expression
wss

See definition df-ss 3588 for more information.

Colors of variables: wff setvar class