Syntax Definition wss 3116

Description: Extend wff notation to include the subclass relation. This is read " A is a subclass of B " or " B includes A". When A exists as a set, it is also read " A is a subset of B".

Hypotheses

Ref	Expression
cA	class A
cB	class B

Assertion

Ref	Expression
wss	wff A C_ B

See definition df-ss 3129 for more information.