Theorem mopick
"At most one" picks a variable value, eliminating an existential
quantifier. (Contributed by NM, 27-Jan-1997.) (Proof shortened by Wolf
Lammen, 17-Sep-2019.)
Conclusion
\( \vdash \exists^\ast x \, \varphi \wedge \exists x \, (\varphi \wedge \psi) \rightarrow \varphi \rightarrow \psi \)
Proof
l0
dfmo
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
l1
sp
\( \vdash \forall x \, (\varphi \rightarrow x = y) \rightarrow \varphi \rightarrow x = y \)
pm3.45
l3
aleximi _
\( \vdash \forall x \, (\varphi \rightarrow x = y) \rightarrow \exists x \, (\varphi \wedge \psi) \rightarrow \exists x \, (x = y \wedge \psi) \)
ax12ev2
\( \vdash \exists x \, (x = y \wedge \psi) \rightarrow x = y \rightarrow \psi \)
syl6 l3 _
\( \vdash \forall x \, (\varphi \rightarrow x = y) \rightarrow \exists x \, (\varphi \wedge \psi) \rightarrow x = y \rightarrow \psi \)
syl5d l1 _
exlimiv _
\( \vdash \exists y \, \forall x \, (\varphi \rightarrow x = y) \rightarrow \exists x \, (\varphi \wedge \psi) \rightarrow \varphi \rightarrow \psi \)
sylbi l0 _
imp _