Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Rohan Ridenour
Shorter primitive equivalent of ax-groth
Grothendieck universes are closed under collection
ccoll
Next ⟩
df-coll
Metamath Proof Explorer
Ascii
Structured
Syntax definition
ccoll
Description:
Extend class notation with the collection operation.
Ref
Expression
Assertion
ccoll
class
(
𝐹
Coll
𝐴
)