Metamath Proof Explorer


Syntax definition ctskm

Description: Extend class definition to include the map whose value is the smallest Tarski class.

Ref Expression
Assertion ctskm class tarskiMap