Metamath Proof Explorer


Syntax definition cif

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

Ref Expression
Assertion cif class if ( 𝜑 , 𝐴 , 𝐵 )