Theorem mo4f

At-most-one quantifier expressed using implicit substitution. Note that the disjoint variable condition on y , ph can be replaced by the nonfreeness hypothesis \( \vdash \Finv y \, \varphi \) with essentially the same proof. (Contributed by NM, 10-Apr-2004.) Remove dependency on [ax-13]. (Revised by Wolf Lammen, 19-Jan-2023.)

Hypotheses
mo4f.1
\( \vdash \Finv x \, \psi \)
mo4f.2
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \forall x \, \forall y \, (\varphi \wedge \psi \rightarrow x = y) \)
Proof
nfv
l1
mo3 _
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \forall x \, \forall y \, (\varphi \wedge [ y / x ] \, \varphi \rightarrow x = y) \)
l2
mo4f.1
mo4f.2
sbiev l2 _
anbi2i _
imbi1i _
2albii _
\( \vdash \forall x \, \forall y \, (\varphi \wedge [ y / x ] \, \varphi \rightarrow x = y) \leftrightarrow \forall x \, \forall y \, (\varphi \wedge \psi \rightarrow x = y) \)
bitri l1 _