Metamath Proof Explorer

Syntax definition chj

Description: Extend class notation with join in CH .

Ref Expression
Assertion chj 
class vH