Understanding Symbolic Logic, Virginia Klenk, Pearson Prentice Hall, 2008, 5th edition, Unit 20, Ex. 3.e

We are asked to prove a theorem. Since the theorem is an equivalence we have to prove each implication separately and then conjoin them. Proving it left to right is not especially challenging, but proving it in the opposite direction requires that we instantiate (y)(Fy ⊃m = y) twice, first into 'y', then into 'x', so that we could set up Modus Ponens arguments inside the scope of the innermost assumption and derive an identity.

{(∃x)Fx • (x)(y)[(Fx • Fy) ⊃x = y]} ≡ (∃x)[Fx • (y)(Fy ⊃x = y)]

1. * (∃x)Fx • (x)(y)[(Fx • Fy) ⊃x = y] / ACP
2. * (∃x)Fx / 1Simp.
3. * Fa / 2EI x/a
4. * (x)(y)[(Fx • Fy) ⊃x = y] / 1Simp.
5. * (y)[(Fa • Fy) ⊃a = y] / 4UI x/a
6. * (Fa • Fy) ⊃a = y / 5UI y/y
7. * ¬ (Fa • Fy) ∨a = y / 6MI
8. * (¬ Fa ∨¬ Fy) ∨a = y / 7DeM
9. * ¬ Fa ∨(¬ Fy ∨a = y) / 8Assoc.
10. * ¬ Fy ∨a = y / 3,9DS
11. * Fy ⊃a = y / 10MI
12. * (y)(Fy ⊃a = y) / 11UG
13. * Fa • (y)(Fy ⊃a = y) / 3,12Conj.
14. * (∃x)[Fx • (y)(Fy ⊃x = y)] / 13EG
15. {(∃x)Fx • (x)(y)[(Fx • Fy) ⊃x = y]} ⊃ (∃x)[Fx • (y)(Fy ⊃x = y)] / 1-14CP
16. * (∃x)[Fx • (y)(Fy ⊃x = y)] / ACP
17. * Fm • (y)(Fy ⊃m = y) / 16EI x/m
18. * Fm / 17Simp.
19. * (y)(Fy ⊃m = y] /17Simp.
20. * * Fx • Fy / ACP
21. * * Fy / 20Simp.
22. * * Fy ⊃m = y / 19UI y/y
23. * * m = y / 21,22MP
24. * * Fx / 20Simp.
25. * * Fx ⊃m = x / 19UI y/x
26. * * m = x / 24,25MP
27. * * x = m / 26Id
28. * * x = y / 23,27Id
29. * (Fx • Fy) ⊃x = y / 20-28CP
30. * (y)[(Fx • Fy) ⊃x = y] / 29UG
31. * (x)(y)[(Fx • Fy) ⊃x = y] / 30UG
32. * (∃x)Fx / 18EG
33. * (∃x)Fx • (x)(y)[(Fx • Fy) ⊃x = y] / 32,31Conj.
34. (∃x)[Fx • (y)(Fy ⊃x = y)] ⊃ (∃x)Fx • (x)(y)[(Fx • Fy) ⊃x = y] / 16-33CP
35. {(∃x)Fx • (x)(y)[(Fx • Fy) ⊃x = y]} ⊃ (∃x)[Fx • (y)(Fy ⊃x = y)] • (∃x)[Fx • (y)(Fy ⊃x = y)] ⊃ (∃x)Fx • (x)(y)[(Fx • Fy) ⊃x = y] / 15,34Conj.
36. {(∃x)Fx • (x)(y)[(Fx • Fy) ⊃x = y]} ≡ (∃x)[Fx • (y)(Fy ⊃x = y)] / 35BE