Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Syntax Definition cn 4093

Description: Extend class notation to include the class of positive integers.

**Assertion**
Ref	Expression
cn

See definition df-n 4423 for more information.

Colors of variables: wff set class