Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Syntax Definition cre 4786

Description: Extend class notation to include real part of a complex number.

**Assertion**
Ref	Expression
cre	class ℜ

See definition df-re 4790 for more information.

Colors of variables: wff set class