Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Syntax Definition cdiv 4091

Description: Extend class notation to include division.

**Assertion**
Ref	Expression
cdiv	class /

See definition df-div 4216 for more information.

Colors of variables: wff set class