AxmExponent (3.13, Axiom): “Exponent”(powerclass of a set is also a set)

AxmExponent (3.13) — “Exponent”(powerclass of a set is also a set)

Morse-Kelley / Von Neumann-Bernays-Gödel class comprehension, sethood, ordinals, Dunaev pairs, cardinals, universes, and reflection.

Num Entity Database Record (Vertical Field Table)

Title	“Exponent”(powerclass of a set is also a set) `#AxmExponent` `#label-exponent-powerclass-of-a-set-is-also-a-set`
Classification	Axiom
Formula	0(∀(X:Class)((X set )→(𝒫(X) set ))) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{X} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{X} \href{../symbols/set-pred.html}{\mathsf{set}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/power-op.html}{\mathcal{P}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/set-pred.html}{\mathsf{set}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PPowSetAx_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])(([X@Class.Expression] set)→(𝒫([X@Class.Expression]) set)))`
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmExponent`) → · (3.13) · `#AxmExponent`