Metamath Proof Explorer


Syntax definition ccj

Description: Extend class notation to include complex conjugate function.

Ref Expression
Assertion ccj class *