Theorem nfmod2

Bound-variable hypothesis builder for the at-most-one quantifier. Usage of this theorem is discouraged because it depends on [ax-13]. See nfmodv for a version replacing the distinctor with a disjoint variable condition, not requiring [ax-13]. (Contributed by Mario Carneiro, 14-Nov-2016.) Avoid [df-eu]. (Revised by BJ, 14-Oct-2022.) (New usage is discouraged.)

Hypotheses
nfmod2.1
\( \vdash \Finv y \, \varphi \)
nfmod2.2
\( \vdash \varphi \wedge \neg \forall x \, x = y \rightarrow \Finv x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, \exists^\ast y \, \psi \)
Proof
l0
dfmo
\( \vdash \exists^\ast y \, \psi \leftrightarrow \exists z \, \forall y \, (\psi \rightarrow y = z) \)
l1
nfv
l2
nfmod2.1
l3
nfmod2.2
nfeqf1
adantl _
nfimd l3 _
nfald2 l2 _
nfexd l1 _
\( \vdash \varphi \rightarrow \Finv x \, \exists z \, \forall y \, (\psi \rightarrow y = z) \)
nfxfrd l0 _