Renaming of Quantified Variables

Law

$Qx,F\equiv Qy{F}_y^x$ if $y$ does not occur in $F$

Example

$\exists xB(x)⟹\exists x,\forall yF(x,y)$ Can be renamed to: $\exists zB(z)⟹\exists x,\forall yF(x,y)$