Syntax Definition wss 1487

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 1492 for more information.

metamath.org