cond_eq

Definition. cond_eq
if A x y = ⋂{u | (A ∧ u = x) ∨ (¬A ∧ u = y)}

The conditional expression, i.e., if A then x else y. See cond_eql and cond_eqr.