Metamath Proof Explorer


Syntax definition cif

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

Ref Expression
Assertion cif class if φ A B