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 don't require that and be
distinct: if
they aren't, 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 2016.
Other variants of this theorem are dvelimf 2015 (with no distinct variable
restrictions) and dvelimALT 2010 (that avoids ax-10 1505). (Contributed by
NM, 23-Nov-1994.) |