Syntax Definition cpw 2398

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 2399 for more information.

Copyright terms: Public domain