Metamath Proof Explorer

Syntax definition ccomlaw

Description: Extend class notation for the commutative law.

Ref Expression
Assertion ccomlaw 
class comLaw