Description: This theorem can be used
to eliminate a distinct variable restriction on
and and replace it with the "distinctor"
as an antecedent. normally has free and can be read
(), and substitutes for and can be read
(). We do not
require that and 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.xA., conjoin them, and apply dvelimdf2077.
Other variants of this theorem are dvelimh2078 (with no distinct variable
restrictions) and dvelimhw1955 (that avoids ax-131999). (Contributed by