How a set whose existence is guarantied by one formula can be substituted into another formula? I try to combine the Power Set Axiom and the Axiom Schema of Specification to prove that for any given set there exist another set that contains the given one as its only element. Moreover, I would like to do it as formal / strict as possible.
So, I start from the following two statements:
$\forall X : \exists P : \forall p : [(p \in P) \Leftrightarrow (p \subseteq X)]$
$\forall X : \forall B : \exists Y : \forall y : [(y \in Y) \Leftrightarrow ((y \in B) \wedge (y = X))]$
One can think of these two statements as "functions". In the first case we take a set X and for this set we can "generate" set P. In the second case we take sets X and B and "generate" set Y. Now I want to combine these "functions". In more details, in the second formula for all X I would like to use its P (as defined by the first formula) instead of B. Or, in other words, in the second formula for any X, I can use any B and I decided to use P as B.
So, the first part of my question is: How can I substitute B by P formally? In other words, how can I write P instead of B in the second formula such that P comes in there together with its definition provided by the first formula?
The second part of my question (assuming that we can write a formula described by the first part of the question) is if we can make such step-by-step transformations of this formula to get the following formula:
$\forall X : \exists Y : \forall y : [(y \in Y) \Leftrightarrow (y = X)]$
 A: This is accomplished via existential instantiation, with universal instantiation also playing a key role in the proof.
Specifically, we reason as follows:

*

*Introduce a symbol $u$ standing for an arbitrary set; we want to show, using the $\mathsf{ZFC}$ axioms, that $\exists Z\forall z(z\in Z\leftrightarrow z=u)$. If we can do this we'll apply universal generalization to conclude $\forall X\exists Z\forall z(z\in Z\leftrightarrow z=X)$ as desired.


*By powerset and universal instantiation, we get $\exists P\forall p(p\in P\leftrightarrow p\subseteq u)$.


*Now we apply existential instantiation: this lets us introduce a new symbol $v$ and the formula $\forall p(p\in v\leftrightarrow p\subseteq u)$.


*And this $v$ we can plug directly into an instance of the separation scheme as desired, via - again - universal instantiation.
Of course there are many different proof systems out there (e.g. compare natural deduction and Hilbert systems), but the above sketch will go through with only minor elaboration in any of them that I'm aware of.
