Symbolic Logic, Dale Jacquette, Wadsworth, 2001, Chpt. 8, Ex. III, problem 15

The task is to prove the tautology:├ (∃x)[(Fx • ¬ Gx) ∨¬ Gx] ⊃(∃y)[(Fy ∨¬ Gy) • ¬ Gy].

1. ├ (∃x)[(Fx • ¬ Gx) ∨¬ Gx] ⊃(∃y)[(Fy ∨¬ Gy) • ¬ Gy]
2. * (∃x)[(Fx • ¬ Gx) ∨¬ Gx] / ACP
3. * * ¬ (∃y)[(Fy ∨¬ Gy) • ¬ Gy] / AIP
4. * * (y)[(Fy ∨¬ Gy) ⊃Gy] / 3QC
5. * * (Fa • ¬ Ga) ∨¬ Ga / 2EI x/a
6. * * (Fa ∨¬ Ga) • (¬ Ga ∨¬ Ga) / 5DeM
7. * * ¬ Ga / 6Simp.
8. * * Fa ∨¬ Ga / 6Simp.
9. * * (Fa ∨¬ Ga) ⊃Ga / 4UI y/a
10. * * Ga / 8,9MP
11. * * Ga • ¬ Ga / 10,7Conj.
12. * ¬ ¬ (∃y)[(Fy ∨¬ Gy) • ¬ Gy] /IP
13. * (∃y)[(Fy ∨¬ Gy) • ¬ Gy] / 12DN
14. (∃x)[(Fx • ¬ Gx) ∨¬ Gx] ⊃(∃y)[(Fy ∨¬ Gy) • ¬ Gy]