Theorem eu6im
One direction of eu6 needs fewer axioms. (Contributed by Wolf Lammen,
2-Mar-2023.)
Conclusion
\( \vdash \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \rightarrow \exists{!} x \, \varphi \)
Proof
exsbim
l1
anim1i _
\( \vdash \exists y \, \forall x \, (x = y \rightarrow \varphi) \wedge \exists z \, \forall x \, (\varphi \rightarrow x = z) \rightarrow \exists x \, \varphi \wedge \exists z \, \forall x \, (\varphi \rightarrow x = z) \)
l2
eu6lem
\( \vdash \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \exists y \, \forall x \, (x = y \rightarrow \varphi) \wedge \exists z \, \forall x \, (\varphi \rightarrow x = z) \)
eu3v
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists z \, \forall x \, (\varphi \rightarrow x = z) \)
3imtr4i l1 l2 _