Theorem 2exeu
Double existential uniqueness implies double unique existential
quantification. The converse does not hold. Usage of this theorem is
discouraged because it depends on [ax-13]. Use the weaker 2exeuv when
possible. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Mario
Carneiro, 22-Dec-2016.) (New usage is discouraged.)
Conclusion
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \rightarrow \exists{!} x \, \exists{!} y \, \varphi \)
Proof
l0
eumo
\( \vdash \exists{!} x \, \exists y \, \varphi \rightarrow \exists^\ast x \, \exists y \, \varphi \)
euex
moimi _
\( \vdash \exists^\ast x \, \exists y \, \varphi \rightarrow \exists^\ast x \, \exists{!} y \, \varphi \)
l3
syl l0 _
2euex
l5
anim12ci l3 _
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \rightarrow \exists x \, \exists{!} y \, \varphi \wedge \exists^\ast x \, \exists{!} y \, \varphi \)
df-eu
\( \vdash \exists{!} x \, \exists{!} y \, \varphi \leftrightarrow \exists x \, \exists{!} y \, \varphi \wedge \exists^\ast x \, \exists{!} y \, \varphi \)
sylibr l5 _