The Logic Book, M. Bergmann, J. Moor, J. Nelson, McGraw Hill, 2004, 10.5E, problem 3f, p. 563

We are asked to show that the following statement is a theorem in predicate logic: (x)(∃y)(Ax ∨By) ≡ (∃y)(x)(Ax ∨By). Under Claim 1 we cannot just drop the quantifiers and restore them in reverse order because of the restriction saying that if every x is in a relation to some y, it doesn't follow that there is a y such that every x is in this relation to it. We are not bound by such a restriction under Claim 2.

1. (x)(∃y)(Ax ∨By) ≡ (∃y)(x)(Ax ∨By)
2. Claim 1: (x)(∃y)(Ax ∨By) ⊃ (∃y)(x)(Ax ∨By)
3. * (x)(∃y)(Ax ∨By) ......... ACP
4. * * ¬ (∃y)(x)(Ax ∨By) ......... AIP
5. * * (y)(∃x)(¬ Ax • ¬ By) ......... 4CQ
6. * * (∃y)(Ax ∨By) ......... 2UI x/x
7. * * Ax ∨Bm ......... 6EI y/m
8. * * (∃x)(¬ Ax • ¬ Bm) ......... 5UI y/m
9. * * ¬ Aa • ¬ Bm ......... 8EI x/a
10. * * ¬ Bm ......... 8Simp.
11. * * Ax ......... 10,7DS
12. * * ¬ Aa ......... 8Simp.
13. * * (y)Ay ......... 11UG
14. * * (∃y) ¬ Ay ......... 12EG
15. * * ¬ Ar ......... 14EI y/r
16. * * Ar ......... 13UI y/r
17. * * Ar • ¬ Ar ......... 16,15Conj.
18. * ¬ ¬ (∃y)(x)(Ax ∨By) ......... 4-17IP
19. * (∃y)(x)(Ax ∨By) ......... 18DN
20. (x)(∃y)(Ax ∨By) ⊃ (∃y)(x)(Ax ∨By) ......... 3-19CP
21. Claim 2: (∃y)(x)(Ax ∨By) ⊃(x)(∃y)(Ax ∨By)
22. * (∃y)(x)(Ax ∨By) ......... ACP
23. * (x)(Ax ∨Bm) ......... 22EI y/m
24. * Ax ∨Bm ......... 23UI x/x
25. * (∃y)(Ax ∨By) ......... 24EG
26. * (x)(∃y)(Ax ∨By) ......... 25UG
27. (∃y)(x)(Ax ∨By) ⊃(x)(∃y)(Ax ∨By) ......... 22-26CP
28. {(x)(∃y)(Ax ∨By) ⊃ (∃y)(x)(Ax ∨By)} • {(∃y)(x)(Ax ∨By) ⊃(x)(∃y)(Ax ∨By)} ......... 20,27Conj.
29. (x)(∃y)(Ax ∨By) ≡ (∃y)(x)(Ax ∨By) ......... 28BE