Syntax Definition cpw 3723

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

Hypothesis

Ref	Expression
cA	class A

Assertion

Ref	Expression
cpw	class ℘A

See definition df-pw 3725 for more information.