Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Rohan Ridenour
Shorter primitive equivalent of ax-groth
Grothendieck universes are closed under collection
cscott
Next ⟩
df-scott
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
cscott
Description:
Extend class notation with the Scott's trick operation.
Ref
Expression
Assertion
cscott
class
Scott
A