Theorem eu2
An alternate way of defining existential uniqueness. Definition 6.10 of
[TakeutiZaring] p. 26. (Contributed by NM, 8-Jul-1994.) (Proof
shortened by Wolf Lammen, 2-Dec-2018.)
Hypothesis
eu2.nf
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \forall x \, \forall y \, (\varphi \wedge [ y / x ] \, \varphi \rightarrow x = y) \)
Proof
l0
df-eu
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists^\ast x \, \varphi \)
eu2.nf
mo3 _
anbi2i _
\( \vdash \exists x \, \varphi \wedge \exists^\ast x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \forall x \, \forall y \, (\varphi \wedge [ y / x ] \, \varphi \rightarrow x = y) \)
bitri l0 _