Syntax Definition cif 3526

Description: Extend class notation to include the conditional operator. See df-if 3527 for a description. (In older databases this was denoted "ded".)

Hypotheses

Ref	Expression
wph	wff 𝜑
cA	class 𝐴
cB	class 𝐵

Assertion

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

See definition df-if 3527 for more information.