Theorem eu1
An alternate way to express uniqueness used by some authors. Exercise
2(b) of [Margaris] p. 110. (Contributed by NM, 20-Aug-1993.) (Revised
by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen,
29-Oct-2018.) Avoid [ax-13]. (Revised by Wolf Lammen, 7-Feb-2023.)
Hypothesis
eu1.nf
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, (\varphi \wedge \forall y \, ([ y / x ] \, \varphi \rightarrow x = y)) \)
Proof
nfs1v
l1
euf _
\( \vdash \exists{!} y \, [ y / x ] \, \varphi \leftrightarrow \exists x \, \forall y \, ([ y / x ] \, \varphi \leftrightarrow y = x) \)
eu1.nf
l3
sb8euv _
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists{!} y \, [ y / x ] \, \varphi \)
eu1.nf
l5
sb6rfv _
equcom
imbi2i _
albii _
l9
anbi12ci l5 _
\( \vdash \varphi \wedge \forall y \, ([ y / x ] \, \varphi \rightarrow x = y) \leftrightarrow \forall y \, ([ y / x ] \, \varphi \rightarrow y = x) \wedge \forall y \, (y = x \rightarrow [ y / x ] \, \varphi) \)
albiim
\( \vdash \forall y \, ([ y / x ] \, \varphi \leftrightarrow y = x) \leftrightarrow \forall y \, ([ y / x ] \, \varphi \rightarrow y = x) \wedge \forall y \, (y = x \rightarrow [ y / x ] \, \varphi) \)
bitr4i l9 _
exbii _
\( \vdash \exists x \, (\varphi \wedge \forall y \, ([ y / x ] \, \varphi \rightarrow x = y)) \leftrightarrow \exists x \, \forall y \, ([ y / x ] \, \varphi \leftrightarrow y = x) \)
3bitr4i l1 l3 _