Theorem nfeu

Bound-variable hypothesis builder for the unique existential quantifier. Note that \( x \) and \( y \) need not be disjoint. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker nfeuw when possible. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.)

Hypothesis
nfeu.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \Finv x \, \exists{!} y \, \varphi \)
Proof
l0
nftru
nfeu.1
a1i _
nfeud l0 _
mptru _