Theorem nfmo

Bound-variable hypothesis builder for the at-most-one 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 nfmov when possible. (Contributed by NM, 9-Mar-1995.) (New usage is discouraged.)

Hypothesis
nfmo.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \Finv x \, \exists^\ast y \, \varphi \)
Proof
l0
nftru
nfmo.1
a1i _
nfmod l0 _
mptru _