Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Uniqueness and unique existence
Unique existence: the unique existential quantifier
euex
Metamath Proof Explorer
Description: Existential uniqueness implies existence. (Contributed by NM , 15-Sep-1993) (Proof shortened by Andrew Salmon , 9-Jul-2011) (Proof
shortened by Wolf Lammen , 4-Dec-2018) (Proof shortened by BJ , 7-Oct-2022)

Ref
Expression
Assertion
euex
$${\u22a2}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi}\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi}$$

Proof
Step
Hyp
Ref
Expression
1
df-eu
$${\u22a2}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi}\leftrightarrow \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi}\wedge {\exists}^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi}\right)$$
2
1
simplbi
$${\u22a2}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi}\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi}$$