Metamath Proof Explorer

Syntax definition cpj1

Description: Extend class notation with left projection.

Ref Expression
Assertion cpj1 class proj1