Theorem nfeudw

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.) Avoid [ax-13]. (Revised by GG, 10-Jan-2024.)

Hypotheses
nfeudw.1
\( \vdash \Finv y \, \varphi \)
nfeudw.2
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, \exists{!} y \, \psi \)
Proof
l0
df-eu
\( \vdash \exists{!} y \, \psi \leftrightarrow \exists y \, \psi \wedge \exists^\ast y \, \psi \)
l1
nfeudw.1
nfeudw.2
l3
nfexd l1 _
l4
nfeudw.1
nfeudw.2
nfmodv l4 _
nfand l3 _
\( \vdash \varphi \rightarrow \Finv x \, (\exists y \, \psi \wedge \exists^\ast y \, \psi) \)
nfxfrd l0 _