Theorem nfeud

Bound-variable hypothesis builder for the unique existential quantifier. Deduction version of nfeu. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker nfeudw when possible. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.)

Hypotheses
nfeud.1
\( \vdash \Finv y \, \varphi \)
nfeud.2
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, \exists{!} y \, \psi \)
Proof
l0
nfeud.1
nfeud.2
adantr _
nfeud2 l0 _