Metamath Proof Explorer


Syntax definition cpr

Description: Extend class notation to include unordered pair.

Ref Expression
Assertion cpr
class { A , B }