Metamath Proof Explorer


Syntax definition cpr

Description: Extend class notation to include unordered pair.

Ref Expression
Assertion cpr class { 𝐴 , 𝐵 }