# Metamath Proof Explorer

## Theorem wl-eutf

Description: Closed form of eu6 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020)

Ref Expression
Assertion wl-eutf ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 nfnae ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
2 nfa1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
3 1 2 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
4 nfnae ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
5 nfnf1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
6 5 nfal ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
7 4 6 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
8 simpl ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
9 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
10 9 adantl ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
11 3 7 8 10 wl-eudf ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)$