Deduction, Daniel Bonevac, Blackwell Publishing, 2nd edition, 2003, Ex. 8.3, problem 13

As elsewhere in this set of problems, the task is to show that the formula (∃x)(y)(x = y ≡ Gy) implies the conclusion of the argument reproduced below. Since the conclusion itself is a biconditional, we show first that the formula on the left implies the formula on the right, and then the reverse. We are free to use the same constants from line 18 on as in the first assumption because that assumption has been discharged on line 17.

1. (∃x)(y)(x = y ≡ Gy)
2. ∴(∃x)(Gx • Fxx) ≡ (∃x)(∃y)(Gx • Gy • Fxy)
3. * (∃x)(Gx • Fxx) / ACP
4. * Ga • Faa / 3EI x/a
5. * (y)(h = y ≡ Gy) / 1EI x/h
6. * h = a ≡ Ga / 5UI y/a
7. * (h = a ⊃ Ga) • (Ga ⊃h = a) / 6BE
8. * Ga / 4Simp.
9. * Ga ⊃h = a / 8Simp.
10. * h = a / 8,9MP
11. * Faa / 4Simp.
12. * Fah / 10,11Id
13. * Gh / 10,8Id
14. * Ga • Gh •Fah / 9,12,13Conj.
15. * (∃y)(Ga • Gy • Fay) / 14EG
16. * (∃x)(∃y)(Gx • Gy • Fxy) / 15EG
17. (∃x)(Gx • Fxx) ⊃(∃x)(∃y)(Gx • Gy • Fxy) / 3-16CP
18. * (∃x)(∃y)(Gx • Gy • Fxy) / ACP
19. * (∃y)(Ga • Gy • Fay) / 18EI x/a
20. * Ga • Gm • Fam / 19EI y/m
21. * (y)(h = y ≡ Gy) / 1EI x/h
22. * h = a ≡ Ga / 21UI y/a
23. * (h = a ⊃ Ga) • (Ga ⊃h = a) / 22BE
24. * Ga ⊃h = a / 23Simp.
25. * Ga / 20Simp.
26. * h = a / 24,25MP
27. * h = m ≡ Gm / 21UI y/m
28. * (h = m ⊃ Gm) • (Gm ⊃h = m) / 27BE
29. * Gm / 20Simp.
30. * Gm ⊃h = m / 28Simp.
31. * h = m / 29,30MP
32. * m = h / 31Id
33. * m = a / 32,26Id
34. * Fam / 20Simp.
35. * Faa / 33,34Id
36. * Ga • Faa / 25,35Conj.
37. * (∃x)(Gx • Fxx) / 36EG
38. (∃x)(∃y)(Gx • Gy • Fxy) ⊃ (∃x)(Gx • Fxx) / 18-37CP
39. [(∃x)(Gx • Fxx) ⊃(∃x)(∃y)(Gx • Gy • Fxy)] • [(∃x)(∃y)(Gx • Gy • Fxy) ⊃ (∃x)(Gx • Fxx)] / 17,38Conj.
40. (∃x)(Gx • Fxx) ≡ (∃x)(∃y)(Gx • Gy • Fxy) / 39BE