Understanding Symbolic Logic, Virginia Klenk, 5th edition, Pearson Prentice Hall, 2008, Unit 20, Ex. 2(c), p.381

The task: construct the proof for the following argument.

1. (∃x){Ax• (y)(Ay ⊃ x=y) • (∃z)[Bz • (w)(Bw ⊃z=w) • z=x]}
2. Ba
3. ∴(x)(Ax ⊃ x=a)
4. * Ax ......... ACP
5. * Am • (y)(Ay ⊃ m=y) • (∃z)[Bz • (w)(Bw ⊃ z=w) • z=m]} ......... 1 EI x/m
6. * (y)(Ay ⊃ m=y) ......... 5 Simp.
7. * Ax ⊃ m=x ......... 6 UI y/x
8. * m=x ......... 4,7 MP
9. * (∃z)[Bz • (w)(Bw ⊃ z=w) • z=m] ......... 5 Simp.
10. * Br • (w)(Bw ⊃ r=w) • r=m ......... 9 EI z/r
11. * (w)(Bw ⊃ r=w) ......... 10 Simp.
12. * Ba ⊃ r=a ......... 11 UI w/a
13. * r = a ......... 2,12 MP
14. * r = m ......... 10 Simp.
15. * m = r ......... 14 Comm.
16. * m = a ......... 15,13 Id
17. * x = m ......... 8 Comm.
18. * x = a ......... 17,16 Id
19. Ax ⊃ x=a ......... 4-18 CP
20. (x)(Ax ⊃ x=a) ......... 19 UG