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
Ascii
Unicode
Syntax definition
cdiag2
Description:
Syntax for the diagonal of the Cartesian square of a set.
Ref
Expression
Assertion
cdiag2
Could not format assertion : No typesetting found for class _Id with typecode class