Syntax Definition cif 1776

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

Hypotheses

Ref	Expression
wph	wff φ
cA	class A
cB	class B

Assertion

Ref	Expression
cif	class if(φ, A, B)

See definition df-if 1777 for more information.

metamath.org