# Metamath Proof Explorer

## Theorem dvelim

Description: This theorem can be used to eliminate a distinct variable restriction on x and z and replace it with the "distinctor" -. A. x x = y as an antecedent. ph normally has z free and can be read ph ( z ) , and ps 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.)

Ref Expression
Hypotheses dvelim.1 ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
dvelim.2 ${⊢}{z}={y}\to \left({\phi }↔{\psi }\right)$
Assertion dvelim ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 dvelim.1 ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 dvelim.2 ${⊢}{z}={y}\to \left({\phi }↔{\psi }\right)$
3 ax-5 ${⊢}{\psi }\to \forall {z}\phantom{\rule{.4em}{0ex}}{\psi }$
4 1 3 2 dvelimh ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$