Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Extended real and complex numbers, real and complex projective lines
Functionalized identity (diagonal in a Cartesian square)
cdiag2
Next ⟩
df-bj-diag
Metamath Proof Explorer
Unicode
Structured
Syntax definition
cdiag2
Description:
Syntax for the diagonal of the Cartesian square of a set.
Ref
Expression
Assertion
cdiag2
class _Id