This theorem can be used to eliminate a distinct variable restriction on \( x \) and \( z \) and replace it with the "distinctor" \( \neg \forall x \, x = y \) as an antecedent. \( \varphi \) normally has \( z \) free and can be read ph ( z ), and \( \psi \) substitutes \( y \) for \( z \) and can be read ph ( y ). We do not require that \( x \) and \( y \) be distinct: if they are not, the distinctor will become false (in multiple-element domains of discourse) and "protect" the consequent.

To obtain a closed-theorem form of this inference, prefix the hypotheses with A. x A. z, conjoin them, and apply dvelimdf.

Other variants of this theorem are dvelimh (with no distinct variable restrictions) and dvelimhw (that avoids [ax-13] ). Usage of this theorem is discouraged because it depends on [ax-13]. Check out dvelimhw for a version requiring fewer axioms. (Contributed by NM, 23-Nov-1994.) (New usage is discouraged.)