# Metamath Proof Explorer

## Theorem dvelimf-o

Description: Proof of dvelimh that uses ax-c11 but not ax-c15 , ax-c11n , or ax-12 . Version of dvelimh using ax-c11 instead of axc11 . (Contributed by NM, 12-Nov-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses dvelimf-o.1 ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
dvelimf-o.2 ${⊢}{\psi }\to \forall {z}\phantom{\rule{.4em}{0ex}}{\psi }$
dvelimf-o.3 ${⊢}{z}={y}\to \left({\phi }↔{\psi }\right)$
Assertion dvelimf-o ${⊢}¬\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 dvelimf-o.1 ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 dvelimf-o.2 ${⊢}{\psi }\to \forall {z}\phantom{\rule{.4em}{0ex}}{\psi }$
3 dvelimf-o.3 ${⊢}{z}={y}\to \left({\phi }↔{\psi }\right)$
4 hba1-o ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)$
5 ax-c11 ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\right)$
6 5 aecoms-o ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\right)$
7 4 6 syl5 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\right)$
8 7 a1d ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\right)\right)$
9 hbnae-o ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}$
10 hbnae-o ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
11 9 10 hban ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
12 hbnae-o ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}$
13 hbnae-o ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
14 12 13 hban ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
15 ax-c9 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({z}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{z}={y}\right)\right)$
16 15 imp ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to \left({z}={y}\to \forall {x}\phantom{\rule{.4em}{0ex}}{z}={y}\right)$
17 1 a1i ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to \left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
18 14 16 17 hbimd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to \left(\left({z}={y}\to {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\right)$
19 11 18 hbald ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\right)$
20 19 ex ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\right)\right)$
21 8 20 pm2.61i ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)\right)$
22 2 3 equsalh ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)↔{\psi }$
23 22 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\to {\phi }\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }$
24 21 22 23 3imtr3g ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$