Theorem nfeud2

Bound-variable hypothesis builder for uniqueness. (Contributed by Mario Carneiro, 14-Nov-2016.) (Proof shortened by Wolf Lammen, 4-Oct-2018.) (Proof shortened by BJ, 14-Oct-2022.) Usage of this theorem is discouraged because it depends on [ax-13]. Use nfeudw instead. (New usage is discouraged.)

Hypotheses
nfeud2.1
\( \vdash \Finv y \, \varphi \)
nfeud2.2
\( \vdash \varphi \wedge \neg \forall x \, x = y \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
nfeud2.1
nfeud2.2
l3
nfexd2 l1 _
l4
nfeud2.1
nfeud2.2
nfmod2 l4 _
nfand l3 _
\( \vdash \varphi \rightarrow \Finv x \, (\exists y \, \psi \wedge \exists^\ast y \, \psi) \)
nfxfrd l0 _