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