Metamath Proof Explorer

Theorem nfeudw

Description: Bound-variable hypothesis builder for the unique existential quantifier. Deduction version of nfeu . Version of nfeud with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 15-Feb-2013) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses nfeudw.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
nfeudw.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
Assertion nfeudw ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{\psi }$

Proof

Step Hyp Ref Expression
1 nfeudw.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfeudw.2 ${⊢}{\phi }\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 nfexd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\psi }$
5 1 2 nfmodv ${⊢}{\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 }$