Metamath Proof Explorer
Table of Contents - 20.16.6.3. Functionalized identity (diagonal in a Cartesian square)
This subsection defines a functionalized version of the identity relation,
that can also be seen as the diagonal in a Cartesian square).
As explained in df-bj-diag, it will probably be deleted.
- cdiag2
- df-bj-diag
- bj-diagval
- bj-diagval2
- bj-eldiag
- bj-eldiag2