cuz - Metamath Proof Explorer

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

Syntax Definition cuz 12511

Description: Extend class notation with the upper integer function. Read "ℤ_≥‘𝑀 " as "the set of integers greater than or equal to 𝑀".

**Assertion**
Ref	Expression
cuz	class ℤ_≥

See definition df-uz 12512 for more information.

Colors of variables: wff setvar class