proof that weak axiom of pairing and axiom schema of specification imply axiom of pairing

Question

as the title says I am trying to give a (nearly, but not fully formal) proof that the weak axiom of pairing (i.e. $\forall x \forall y \exists p: x \in p \wedge y \in p$) together with a suitable instance of the axiom schema of specification does imply the axiom of pairing. I haven't found a suitable instance yet, so this would be the first step to take.

Answer 1

Here is a 'nearly, but not fully, formal proof' (OK, it is fully formal, but it is not fully completed):

Answer 2

Given $x,y$, let $p$ be such that $x\in p\land y\in p$. Then $\{x,y\}=\{\,t\in p\mid t=x\lor t=y\,\}$.

Answer 3

Fix $x,y$ and take $p$ such that $x, y \in p$. Now take the formula $\Phi = ( z = x \lor z = y)$ and apply the axiom of specification on $p$.