Proposition: If $\psi$ is a subformula of $\phi$ and $\phi'$ results from replacing $0$ or more occurs of $\psi$ in $\phi$ per a well formed formula $\rho$ and each free variable of $\psi$ and $\rho$ that it's also a bound variable of $\phi$ occurs in the list $y_1,y_2,...,y_k,$ then $$\vdash [\forall y_1...\forall y_k(\psi\leftrightarrow\rho)]\to(\phi\leftrightarrow\phi')$$
My question is how will I know that some variable will occur\appear in that unknow list $y_1,y_2,...,y_k$? Doesn't this list have to have some property?
I don't understand this proposition.
Like most propositions, the one you quoted is intended to be true for all values of the symbols in it. In the present case, this means: For all formulas $\phi,\phi',\psi,\rho$, all natural numbers $k$, and all lists $y_1,\dots,y_k$ of $k$ variables, if the hypothesis of your proposition holds then so does the conclusion.
So you're given that the $y$'s include all the variables that are free in $\psi$ or in $\rho$ and bound in $\phi$; that's part of the hypoothesis. You're not expected to figure out what those $y$'s are.
(By the way, "bounded" in the proposition is a typo; it should be "bound".)