Three examples come to mind, all with $P=ZF$ or some other base theory.

1) [Fermat / Heath-Brown / Zagier][1]:

- $Q$ = "every prime of the form $4n+1$ is the sum of two squares";
- $X$ = "the map
$$(x,y,z)\mapsto
\begin{cases}
(x+2z,~z,~y-x-z),\quad \textrm{if}\,\,\, x < y-z \\
(2y-x,~y,~x-y+z),\quad \textrm{if}\,\,\, y-z < x < 2y\\
(x-2y,~x-y+z,~y),\quad \textrm{if}\,\,\, x > 2y
\end{cases}
$$
 is an involution with an odd number of fixed points on the set $\{(x,y,z)\in\mathbb{N}^3:x^2+4yz=p\}$.

2) [Hadamard / de la Vallee Poussin / Newman / Zagier][2]:

- $Q$ = the prime number theorem;
- $X_1,\ldots,X_7$ = Zagier's statements $I-VI$ and the Analytic Theorem.

3) [Lebesgue / Caratheodory][3]:

- $Q$ = the Lebesgue-measurable sets are closed under countable unions;
- $X$ = the Caratheodory-measurable sets are closed under countable unions.

I think giving the statements $X$ and asking for proofs could be a reasonable homework or group project for a graduate class in Number Theory, Complex Analysis, or Real Analysis, which is saying something given the significance of the $Q$.

  [1]: https://en.wikipedia.org/wiki/Proofs_of_Fermat%27s_theorem_on_sums_of_two_squares#Zagier's_%22one-sentence_proof%22
  [2]: https://people.mpim-bonn.mpg.de/zagier/files/doi/10.2307/2975232/fulltext.pdf
  [3]: https://en.wikipedia.org/wiki/Carath%C3%A9odory%27s_extension_theorem