Database
TG (TARSKI-GROTHENDIECK) SET THEORY
Inaccessibles
Grothendieck universes
cgru
Next ⟩
df-gru
Metamath Proof Explorer
Unicode
Structured
Syntax definition
cgru
Description:
Extend class notation to include the class of all Grothendieck universes.
Ref
Expression
Assertion
cgru
class Univ