# Metamath Proof Explorer

## Theorem nfeud2

Description: Bound-variable hypothesis builder for uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . Check out nfeudw for a version that replaces the distinctor with a disjoint variable condition, not requiring ax-13 . (Contributed by Mario Carneiro, 14-Nov-2016) (Proof shortened by Wolf Lammen, 4-Oct-2018) (Proof shortened by BJ, 14-Oct-2022) (New usage is discouraged.)

Ref Expression
Hypotheses nfeud2.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
nfeud2.2 ${⊢}\left({\phi }\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
Assertion nfeud2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 nfeud2.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfeud2.2 ${⊢}\left({\phi }\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 df-eu ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}{\psi }↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\psi }\wedge {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
4 1 2 nfexd2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\psi }$
5 1 2 nfmod2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{\psi }$
6 4 5 nfand ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}{\psi }\wedge {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
7 3 6 nfxfrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{\psi }$