Syntax Definition cif 2351

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

Hypotheses

Ref	Expression
wph	wff ph
cA	class A
cB	class B

Assertion

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

See definition df-if 2352 for more information.

Copyright terms: Public domain