24.6 Quantifier Reorder (QRe)
This equivalence deals with multiple quantifiers, which you haven’t learned much about yet. We’ll cover that in Chapter 27.
But since it is related to all the other equivalences in this chapter, we mention it here.
AxAyL(x,y) ⇔ AyAxL(x,y)
ExEyL(x,y) ⇔ EyExL(x,y)
Here’s the idea: when you have multiple quantifiers and they are of the same type, then order doesn’t matter. You can reorder them and preserve equivalence.
(Foreshadowing: if the quantifiers are a mixture of universal and existential, then reordering fails.)