Metamath Proof Explorer


Syntax definition bj-c2uple

Description: Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-c2uple
class (| A ,, B |)