Table of Contents - 2.1.15. The conditional operator for classes
This subsection introduces the conditional operator for classes, denoted
by (see df-if). It is the analogue for classes
of the conditional operator for propositions, denoted by
(see df-ifp).