Htykuut

In Angelo Margaris's book First Order Mathematical Logic we have the following theorem (see pp. 84),

The equivalence theorem. Let $U$ and $V$ be two formulas (of First Order Predicate Calculus). Let $P_U$ be a formula in which $U$ occurs as a subformula. Let $P_V$ denote the result of replacing some occurrences of $U$ by $V$. Let every variable that is free in $U$ or $V$ and bound in $P_U$ be in the list $v_1,…,v_k$. Then, $$⊢∀v_1…∀v_k(Uleftrightarrow V)→(P_Uleftrightarrow P_V)$$

My questions

1. What is(are) the reason(s) for including "Let every variable that is free in $U$ or $V$ and bound in $P_U$ be in the list $v_1,…,v_k$.." in the statement of the result?



2. 
   

   What would be the problem(s) in the following claim,

   
   
   

   
   

   Let $U$ and $V$ be two formulas (of First Order Predicate Calculus). Let $P_U$ be a formula in which $U$ occurs as a subformula. Let $P_V$ denote the result of replacing some occurrences of $U$ by $V$. Then, $$⊢∀w(Uleftrightarrow V)→(P_Uleftrightarrow P_V)$$for any variable $w$.

   
   

   
   
   

   Is this claim wrong? Can anyone give me an example?

   
   



3. One answer to the first question obviously is to go through the proof of the theorem and see whether they use the assumption anywhere in the proof. Well, in the proof the assumption is used only to prove that $v$ is bound in $∀v_1…∀v_k(Uleftrightarrow V)$ if $P_U$ is of the form $forall v Q_U$. Is this the only way to prove that $v$ is bound in $∀v_1…∀v_k(Uleftrightarrow V)$?