Theorem nfmod

Bound-variable hypothesis builder for the at-most-one quantifier. Deduction version of nfmo. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker nfmodv when possible. (Contributed by Mario Carneiro, 14-Nov-2016.) (New usage is discouraged.)

Hypotheses
nfmod.1
\( \vdash \Finv y \, \varphi \)
nfmod.2
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, \exists^\ast y \, \psi \)
Proof
l0
nfmod.1
nfmod.2
adantr _
nfmod2 l0 _