Metamath Proof Explorer


Syntax definition cif

Description: Extend class notation to include the conditional operator for classes.

Ref Expression
Assertion cif
class if ( ph , A , B )