# Metamath Proof Explorer

## Theorem dvelimf

Description: Version of dvelimv without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 1-Oct-2002) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 11-May-2018) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 dvelimf.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 dvelimf.2 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\psi }$
3 dvelimf.3 ${⊢}{z}={y}\to \left({\phi }↔{\psi }\right)$
4 2 3 equsal ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)↔{\psi }$
5 4 bicomi ${⊢}{\psi }↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)$
6 nfnae ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
7 nfeqf ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}={y}$
8 7 ancoms ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}={y}$
9 1 a1i ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
10 8 9 nfimd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)$
11 6 10 nfald2 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)$
12 5 11 nfxfrd ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$