Theorem exists2
A condition implying that at least two things exist. (Contributed by
NM, 10-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Reduce axiom usage. (Revised by Wolf Lammen, 4-Mar-2023.)
Conclusion
\( \vdash \exists x \, \varphi \wedge \exists x \, \neg \varphi \rightarrow \neg \exists{!} x \, x = x \)
Proof
l0
ax-5
\( \vdash \forall x \, x = y \rightarrow \forall x \, \forall x \, x = y \)
l1
ax-5
\( \vdash \forall x \, \varphi \rightarrow \forall x \, \forall x \, \varphi \)
l2
axc16
\( \vdash \forall x \, x = y \rightarrow \varphi \rightarrow \forall x \, \varphi \)
l3
exlimdh l0 l1 _
l4
com12 _
\( \vdash \exists x \, \varphi \rightarrow \forall x \, x = y \rightarrow \forall x \, \varphi \)
l5
exists1
\( \vdash \exists{!} x \, x = x \leftrightarrow \forall x \, x = y \)
l6
alex
l7
bicomi _
\( \vdash \neg \exists x \, \neg \varphi \leftrightarrow \forall x \, \varphi \)
l8
3imtr4g l4 l5 _
l9
con2d _
l10
imp _