This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Syntax definition cpw

Description: Extend class notation to include power class. (The tilde in the Metamath token is meant to suggest the calligraphic font of the P.)

		Ref	Expression
	Assertion	cpw	class 𝒫 𝐴