Syntax Definition wss 3258

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 ⊆ B

See definition df-ss 3260 for more information.