Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BTernaryTau
ZF set theory
The constructible universe
ck2
Next ⟩
ck3
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
ck2
Description:
Extend the definition of a class to include the second argument of the
_J
function.
Ref
Expression
Assertion
ck2
Could not format assertion : No typesetting found for class _K2 with typecode class