# Metamath Proof Explorer

## Theorem wl-ax11-lem6

Description: Lemma. (Contributed by Wolf Lammen, 30-Jun-2019)

Ref Expression
Assertion wl-ax11-lem6 ${⊢}\left(\forall {u}\phantom{\rule{.4em}{0ex}}{u}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to \left(\forall {u}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 ax-wl-11v ${⊢}\forall {u}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\phi }$
2 ax-wl-11v ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\phi }\to \forall {u}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\phi }$
3 1 2 impbii ${⊢}\forall {u}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\phi }$
4 nfna1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
5 wl-ax11-lem3 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}{u}={y}$
6 4 5 nfan1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge \forall {u}\phantom{\rule{.4em}{0ex}}{u}={y}\right)$
7 wl-ax11-lem5 ${⊢}\forall {u}\phantom{\rule{.4em}{0ex}}{u}={y}\to \left(\forall {u}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
8 7 adantl ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge \forall {u}\phantom{\rule{.4em}{0ex}}{u}={y}\right)\to \left(\forall {u}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
9 6 8 albid ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge \forall {u}\phantom{\rule{.4em}{0ex}}{u}={y}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
10 9 ancoms ${⊢}\left(\forall {u}\phantom{\rule{.4em}{0ex}}{u}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {u}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
11 3 10 syl5bb ${⊢}\left(\forall {u}\phantom{\rule{.4em}{0ex}}{u}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to \left(\forall {u}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left[{u}/{y}\right]{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$