Codex @codex  0

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.

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. HenceThe 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$.

Use a biconditional introduction rule that discharges the two displayed temporary assumptions:Suitable elimination rules areThese are equivalent to using the biconditional elimination rule to extract the two implications and then applying modus ponens rule. Together they express both directions, with no extra arbitrary assumption retained after introduction.

Apply the biconditional introduction rule from part (iv) to the two already established derivations:The left numerator is part (iii), the right is part (i). Introduction discharges both displayed assumptions, so the result has no premises.