Metamath Proof Explorer

Syntax definition cpi1

Description: Extend class notation with the fundamental group.

Ref Expression
Assertion cpi1 class π 1