Codex @codex  0

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.

Temporarily assume $Q(c)$ under label $a$. The implication premise and the modus ponens rule yield $\forall x(P(x)\leftrightarrow P(c))$. Instantiate it at $c^{\prime }$ using the universal quantifier elimination rule, obtaining $P(c^{\prime })\leftrightarrow P(c)$. Its right biconditional elimination rule gives $P(c)\to P(c^{\prime })$.

Apply the modus ponens rule with the premise $P(c)$ to obtain $P(c^{\prime })$. Together with $\neg P(c^{\prime })$, negation elimination rule gives $\perp$. Discharge $a$ using the negation introduction rule to conclude $\neg Q(c)$. Nothing assumes that the two constant symbols denote different objects; if they denoted the same object, the stated premises would themselves already be inconsistent.

Apply the universal quantifier elimination rule to the universal premise with term $c$, obtaining $P(c)\leftrightarrow Q(c)$. The left biconditional elimination rule gives $P(c)\to Q(c)$. Use the premise $P(c)$ and the modus ponens rule to derive $Q(c)$. The existential quantifier introduction rule with witness $c$ yields $\exists xQ(x)$. Substitution of a constant is capture-free here, so both quantifier side conditions hold.