Theorem nfmodv

Bound-variable hypothesis builder for the at-most-one quantifier. See nfmod for a version without disjoint variable conditions but requiring [ax-13]. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by BJ, 28-Jan-2023.)

Hypotheses
nfmodv.1
\( \vdash \Finv y \, \varphi \)
nfmodv.2
\( \vdash \varphi \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
nfmodv.1
l3
nfmodv.2
nfvd
nfimd l3 _
nfald l2 _
nfexd l1 _
\( \vdash \varphi \rightarrow \Finv x \, \exists z \, \forall y \, (\psi \rightarrow y = z) \)
nfxfrd l0 _