Deduction, Daniel Bonevac, Blackwell Publishing, 2nd Edition, 2003, chpt. 8.3, problem 15

Show that (∃x)[Gx • (Fx ⊃Ha)] ≡ [(∃x)(Gx • Fx) ⊃Ha] is a consequence of (∃x)(y)(y = x ≡ Gy).

1. (∃x)(y)(y = x ≡ Gy)
2. ∴(∃x)[Gx • (Fx ⊃Ha)] ≡ [(∃x)(Gx • Fx) ⊃Ha]
3. * (∃x)[Gx • (Fx ⊃Ha)] ... ACP
4. * * (∃x)(Gx • Fx) ... ACP
5. * * Gm • Fm ... 4EI x/m
6. * * (y)(y = h ≡ Gy) ... 1EI x/h
7. * * m = h ≡ Gm ... 6UI y/m
8. * * (m = h ⊃Gm) •(Gm ⊃m = h) ... 7BE
9. * * Gm ... 5Simp.
10. * * Gm ⊃m = h ... 8Simp.
11. * * m = h ... 9,10MP
12. * * Gr • (Fr ⊃Ha) ... 3EI x/r
13. * * r = h ≡ Gr ... 6UI y/r
14. * * (r = h ⊃Gr) •(Gr ⊃r = h) ... 13BE
15. * * Gr ... 12Simp.
16. * * Gr ⊃r = h ... 14Simp.
17. * * r = h ... 15,16MP
18. * * h = m ... 11Id.
19. * * r = m ... 17,18Id.
20. * * Fr ⊃Ha ... 12Simp.
21. * * Fm ... 5Simp.
22. * * Fr ... 19,21Id.
23. * * Ha ... 22,20MP
24. * (∃x)(Gx • Fx) ⊃Ha ... 4-23CP
25. [(∃x)[Gx • (Fx ⊃Ha)] ⊃[(∃x)(Gx • Fx) ⊃Ha] ... 3-24CP
26. * (∃x)(Gx • Fx) ⊃Ha ... ACP
27. * * ¬ (∃x)[Gx • (Fx ⊃Ha) ... AIP
28. * * (x)[Gx ⊃(Fx • ¬ Ha) ... 27QC
29. * * (y)(y = m ≡ Gy) ... 1EI x/m
30. * * m = m ≡ Gm ... 29UI y/m
31. * * (m = m ⊃Gm) •(Gm ⊃m = m) ... 30BE
32. * * m = m ⊃Gm ... 31Simp.
33. * * m = m ... Id.
34. * * Gm ... 33,32MP
35. * * Gm ⊃(Fm • ¬ Ha) ... 28UI x/m
36. * * Fm • ¬ Ha ... 34,35MP
37. * * ¬ Ha ... 36Simp.
38. * * Fm ... 36Simp.
39. * * Gm • Fm ... 34,38Conj.
40. * * (∃x)(Gx • Fx) ... 39EG
41. * * Ha ... 26,40MP
42. * * Ha • ¬ Ha ... 41,37Conj.
43. * ¬ ¬ (∃x)[Gx • (Fx ⊃Ha) ... 27-42IP
44. * (∃x)[Gx • (Fx ⊃Ha) ... 43DN
45. [(∃x)(Gx • Fx) ⊃Ha] ⊃[(∃x)[Gx • (Fx ⊃Ha)] ... 26-44CP


46. 
    
    [(∃x)[Gx • (Fx ⊃Ha)] ⊃[(∃x)(Gx • Fx) ⊃Ha] • [(∃x)(Gx • Fx) ⊃Ha] ⊃[(∃x)[Gx • (Fx ⊃Ha)] ... 25,45Conj.


47. 
    
    (∃x)[Gx • (Fx ⊃Ha)] ≡ [(∃x)(Gx • Fx) ⊃Ha] ... 46BE