|Description: This theorem can be used
to eliminate a distinct variable restriction on
and and replace it with the
as an antecedent. normally has free and can be read
substitutes for and can be read
. We do not require that and be
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 , conjoin them, and apply dvelimdf 2050.
Other variants of this theorem are dvelimh 2051 (with no distinct variable
restrictions) and dvelimhw 1902 (that avoids ax-13 1968). (Contributed by