= Solution
Eliminate the existential premise with fresh witness $a$. Its first conjunct gives $Q(a)$ and its second gives $\forall y\,(Q(y)\to y=a)$. For a fresh arbitrary $b$, one direction of the desired <logical biconditional> follows by <universal elimination>. For the other, $b=a$ must be reversed before transporting $Q(a)$ to $Q(b)$ using the supplied oriented <equality elimination rule>.
|| Line
|| Context
|| Formula
|| Justification
| 1
| $\{1\}$
| $\exists x\,(Q(x)\land\forall y\,(Q(y)\to y=x))$
| Premise
| 2
| $\{1,2\}$
| $Q(a)\land\forall y\,(Q(y)\to y=a)$
| Temporary assumption
| 3
| $\{1,2\}$
| $Q(a)$
| <conjunction elimination rule> $\land\text{-elim-L}$ on 2
| 4
| $\{1,2\}$
| $\forall y\,(Q(y)\to y=a)$
| <conjunction elimination rule> $\land\text{-elim-R}$ on 2
| 5
| $\{1,2\}$
| $Q(b)\to b=a$
| <universal elimination> $\forall\text{-elim}$ on 4; instantiate at $b$
| 6
| $\{1,2,6\}$
| $b=a$
| Temporary assumption
| 7
| $\{1,2,6\}$
| $b=b$
| <equality introduction rule> $=\text{-intro}$
| 8
| $\{1,2,6\}$
| $a=b$
| <equality elimination rule> $=\text{-elim}$ on 6, 7
| 9
| $\{1,2,6\}$
| $Q(b)$
| <equality elimination rule> $=\text{-elim}$ on 8, 3
| 10
| $\{1,2\}$
| $b=a\to Q(b)$
| <implication introduction rule> $\to\text{-intro}$ on 9; discharge 6
| 11
| $\{1,2\}$
| $Q(b)\leftrightarrow b=a$
| <biconditional introduction rule> $\leftrightarrow\text{-intro}$ on 5, 10
| 12
| $\{1,2\}$
| $\forall y\,(Q(y)\leftrightarrow y=a)$
| <universal introduction> $\forall\text{-intro}$ on 11; $b$ fresh
| 13
| $\{1,2\}$
| $\exists x\,\forall y\,(Q(y)\leftrightarrow y=x)$
| <existential quantifier introduction rule> $\exists\text{-intro}$ on 12; witness $a$
| 14
| $\{1\}$
| $\exists x\,\forall y\,(Q(y)\leftrightarrow y=x)$
| <existential quantifier elimination rule> $\exists\text{-elim}$ on 1, 13; discharge 2; $a$ fresh
Here $b$ is absent from every open assumption when line 12 uses <universal introduction>. In line 13 the <existential quantifier> binds the witness position occupied by $a$; the conclusion then has no free $a$, allowing line 14 to close its witness subproof. Hence
$$
\boxed{\exists x\,(Q(x)\land\forall y\,(Q(y)\to y=x))\vdash\exists x\,\forall y\,(Q(y)\leftrightarrow y=x).}
$$
The premise says an object satisfying $Q$ exists and every object satisfying $Q$ equals it. The <logical biconditional> adds the converse explicitly: every object equal to that witness also satisfies $Q$.
Back to article page
