In sequent calculus LK, the right quantifier rule is $$ \dfrac{\Gamma\vdash[y\backslash x]A, \Delta}{\Gamma\vdash\forall xA, \Delta}\forall\text{R} $$ where $y$, the eigenvariable, cannot occur free in any lower sequent (the eigenvariable condition).
I don't understand why the eigenvariable, $y$, can never occur free in lower sequents. I see why the eigenvariable condition is necessary immediately after the application of the rule but not in lower sequents. Take for example the following partial deduction: $$ \dfrac{\dfrac{\Gamma\vdash A(x)}{\Gamma\vdash\forall xA(x)}\forall \text{R}\quad\Delta\vdash B(x)}{\Gamma, \Delta\vdash\forall xA(x)\wedge B(x)}\wedge\text{R} $$ where $x$ only occurs in $A$ and $B$.
To me it seems that there's nothing logically wrong with this partial deduction (reading top-down) even though, according to the eigenvariable condition, this is invalid. It seems that the eigenvariable condition only needs to hold up until the next fork in the deduction. What am I missing here?