Understanding Symbolic Logic, Virginia Klenk, Pearson Prentice Hall, 2008, 5th edition, Unit 18, Ex. 1(p), p. 354

Construct a proof for the following argument. Tip: we can't generalize by universal generalization within the scope of an assumption if the assumption contains a free variable on the first line, but we are within our rights to do so by existential generalization (line 20). Then, it is just the question of pushing the negation out, which changes the quantifier to a universal one (line 21).

1. (∃x)[Px • (y)(Sy ⊃Txy)]
2. (x){[Px • ¬ (y)(Wy ⊃Ayx)] ⊃(z)(Bxz ⊃Sz)}
3. (x){Px ⊃¬ (∃y)(Wy • (Txy ∨ Ayx)]}
4. ∴(∃x){Px • (y)[Wy ⊃¬ (Ayx ∨Bxy)]}
5. Pa • (y)(Sy ⊃Tay) / 1EI x/a
6. Pa ⊃¬ (∃y)(Wy • (Tay ∨ Aya) / 3UI x/a
7. Pa / 5Simp.
8. ¬ (∃y)(Wy • (Tay ∨ Aya) / 7,6MP
9. (y)[Wy ⊃¬ (Tay ∨ Aya)] / 8QC
10. * Wy / ACP
11. * Wy ⊃¬ (Tay ∨ Aya) / 9UI y/y
12. * ¬ (Tay ∨ Aya) / 10,11MP
13. * ¬ Tay • ¬ Aya / 12DeM
14. * (y)(Sy ⊃Tay) / 5Simp.
15. * Sy ⊃Tay / 14UI y/y
16. * ¬ Tay / 13Simp.
17. * ¬ Sy / 16,15MT
18. * ¬ Aya / 13Simp.
19. * Wy • ¬ Aya / 10,18Conj.
20. * (∃y)(Wy • ¬ Aya) / 19EG
21. * ¬ (y)(Wy ⊃Aya) / 20QC
22. * Pa • ¬ (y)(Wy ⊃Aya) / 7,21Conj.
23. * [Pa • ¬ (y)(Wy ⊃Aya)] ⊃(z)(Baz ⊃Sz) / 2UI x/a
24. * (z)(Baz ⊃Sz) / 22,23MP
25. * Bay ⊃Sy / 24UI z/y
26. * ¬ Bay / 17,25MT
27. * ¬ Bay • ¬ Aya / 26,18Conj.
28. * ¬ (Bay ∨ Aya) / 27DeM
29. Wy ⊃ ¬ (Bay ∨ Aya) / 10-28CP
30. (y)[Wy ⊃¬ (Aya ∨Bay)] / 29UG
31. Pa • (y)[Wy ⊃¬ (Aya ∨Bay)] / 7,30Conj.
32. (∃x){Px • (y)[Wy ⊃¬ (Ayx ∨Bxy)]} / 31EG