Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BTernaryTau
ZF set theory
The constructible universe
cl
Next ⟩
df-lexo
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
cl
Description:
Extend the definition of a class to include the class of all constructible sets.
Ref
Expression
Assertion
cl
Could not format assertion : No typesetting found for class _L with typecode class