Syntax Definition cpw 3566

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 ~P A

See definition df-pw 3568 for more information.