Understanding Symbolic Logic, Virginia Klenk, Prentice Hall, 2008, Fifth edition, Unit 20, Ex.3e, p.381

Another theorem to prove. The hardest part is to realize that the same expression can be instantiated twice, each time to a different variable, the idea being to set up two identities under the second assumption below and then use the transitive property of identity to derive x = y. It would have been possible to decompose line 6 into a conjunction of two disjunctions and then simplify via disjunctive syllogism but I am too lazy to do that so I have used exportation instead.

Theorem: {(∃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. * Fm / 2EI x/m
4. * (x)(y)[(Fx • Fy) ⊃x = y] / 1Simp.
5. * (y)[(Fm • Fy) ⊃m = y] / 4UI x/m
6. * (Fm • Fy) ⊃m = y / 5UI y/y
7. * Fm ⊃(Fy ⊃m = y) / 6Exp.
8. * Fy ⊃m = y / 3,7MP
9. * (y)(Fy ⊃m = y) / 8UG
10. * Fm • (y)(Fy ⊃m = y) / 3,9Conj.
11. * (∃x)[Fx • (y)(Fy ⊃x = y)] / 10EG
12. {(∃x)Fx • (x)(y)[(Fx • Fy) ⊃x = y]} ⊃ (∃x)[Fx • (y)(Fy ⊃x = y)]
13. * (∃x)[Fx • (y)(Fy ⊃x = y)] / ACP
14. * Fa • (y)(Fy ⊃a = y) / 13EI
15. * (y)(Fy ⊃a = y) / 14Simp.
16. * * Fx • Fy / ACP
17. * * Fy ⊃a = y / 15UI y/y
18. * * Fy / 16Simp.
19. * * a = y / 18,17MP
20. * * Fx ⊃a = x / 15UI y/x
21. * * Fx / 16Simp.
22. * * a = x / 21,20MP
23. * * x = a / 22Id
24. * * x = y / 19,23Id
25. * (Fx • Fy) ⊃x = y / 16-24CP
26. * (y)[(Fx • Fy) ⊃x = y] / 25UG
27. * (x)(y)[(Fx • Fy) ⊃x = y] / 26UG
28. * Fa / 14Simp.
29. * Fa • (x)(y)[(Fx • Fy) ⊃x = y] / 28,27Conj.
30. * (∃x){Fx • (x)(y)[(Fx • Fy) ⊃x = y]} / 29EG
31. (∃x)[Fx • (y)(Fy ⊃x = y)] ⊃(∃x){Fx • (x)(y)[(Fx • Fy) ⊃x = y]} / 13-30CP
32. {{(∃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]}} / 12,31Conj.
33. {(∃x)Fx • (x)(y)[(Fx • Fy) ⊃x = y]} ≡ (∃x)[Fx • (y)(Fy ⊃x = y)] / 32BE