Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
Tuples of classes
bj-c2uple
Next ⟩
df-bj-2upl
Metamath Proof Explorer
Unicode
Structured
Syntax definition
bj-c2uple
Description:
Syntax for Morse couple.
(Contributed by
BJ
, 6-Oct-2018)
Ref
Expression
Assertion
bj-c2uple
class (| A ,, B |)