Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Digital systems, linear algebra, introduction to formal proof / 8 / a / i

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.