Theorem euequ

There exists a unique set equal to a given set. Special case of [eueqi] proved using only predicate calculus. The proof needs \( y' = z \) be free of \( x \). This is ensured by having \( x \) and \( y' \) be distinct. Alternately, a distinctor \( \neg \forall x \, x = y' \) could have been used instead. See [eueq] and [eueqi] for classes. (Contributed by Stefan Allan, 4-Dec-2008.) (Proof shortened by Wolf Lammen, 8-Sep-2019.) Reduce axiom usage. (Revised by Wolf Lammen, 1-Mar-2023.)

Conclusion
\( \vdash \exists{!} x \, x = y' \)
Proof
l0
ax6ev
\( \vdash \exists x \, x = y' \)
l1
ax6ev
\( \vdash \exists z \, z = y' \)
equeuclr
alrimiv _
\( \vdash z = y' \rightarrow \forall x \, (x = y' \rightarrow x = z) \)
l4
eximii l1 _
\( \vdash \exists z \, \forall x \, (x = y' \rightarrow x = z) \)
eu3v
\( \vdash \exists{!} x \, x = y' \leftrightarrow \exists x \, x = y' \wedge \exists z \, \forall x \, (x = y' \rightarrow x = z) \)
mpbir2an l0 l4 _