Table of Contents - 21.38.6.5. _Begriffsschrift_ Chapter II with logical equivalence
Here we leverage df-ifp to partition a wff into two that are disjoint with
the selector wff.
Thus if we are given then we replace
the concept (illegal in our notation ) with
to reason about the values of the "function."
Likewise, we replace the similarly illegal concept with
.