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

Here is an argument which works equally well on the intuitive and on the symbolic level, as 'at least' and 'at most' in relation to the same quantity are simply the long way of saying 'exactly'. Perhaps the trickiest thing here is to realize that we have to instantiate line 2 more than once, first into constants, then into variables, and then again into constants, to free up the desired predicates.

There are at least two pianists in the room. All the pianists in the room are composers. There are at most two composers in the room. Therefore, there are exactly two pianists in the room.

1. (∃x)(∃y)[Px • Py • Rx • Ry • ¬ (x = y)]
2. (x)[(Px • Rx) ⊃ Cx]
3. (x)(y)(z)[(Cx • Cy • Cz • Rx • Ry • Rz) ⊃(z = x ∨z = y ∨y = x)]
4. ∴(∃x)(∃y){Px • Py • Rx • Ry • ¬ (x = y) • (z)[(Pz • Rz) ⊃(z = x ∨z = y)]}
5. (∃y)[Pa • Py • Ra • Ry • ¬ (a = y)] ......... 1 EI x/a
6. Pa • Pm • Ra • Rm • ¬ (a = m) ......... 5 EI y/m
7. (Pa • Ra) ⊃ Ca ......... 2 UI x/a
8. Pa • Ra ......... 6 Simp.
9. Ca ......... 8, 7 MP
10. * Pz • Rz ......... ACP
11. * (y)(z)[(Ca • Cy • Cz • Ra • Ry • Rz) ⊃(z = a ∨z = y ∨y = a)] ......... 3 UI x/a
12. * (z)[(Ca • Cm • Cz • Ra • Rm • Rz) ⊃(z = a ∨z = m ∨m = a)] ......... 11 UI y/m
13. * (Ca • Cm • Cz • Ra • Rm • Rz) ⊃(z = a ∨z = m ∨m = a) ......... 12 UI z/z
14. * (Pz • Rz) ⊃ Cz ........ 2 UI x/z
15. * Cz ......... 10, 14 MP
16. * Pm • Rm ......... 6 Simp.
17. * (Pm • Rm) ⊃ Cm ......... 2 UI x/m
18. * Cm ......... 16, 17 MP
19. * Ra ......... 8 Simp.
20. * Rm ......... 16 Simp.
21. * Rz ......... 10 Simp.
22. * Ca • Cm • Cz • Ra • Rm • Rz ......... 9, 15, 18, 19, 20, 21 Conj.
23. * z = a ∨z = m ∨m = a ......... 13, 22 MP
24. * ¬ (a = m) ......... 6 Simp.
25. * ¬ (m = a) ......... 24 Comm.
26. * z = a ∨z = m ......... 23, 25 DS
27. (Pz • Rz) ⊃ z = a ∨z = m ......... 10-26 CP
28. (z)[(Pz • Rz) ⊃ z = a ∨z = m ] ......... 27 UG
29. Pa • Pm • Ra • Rm • ¬ (a = m) • (z)[(Pz • Rz) ⊃ z = a ∨z = m ] ......... 6, 28 Conj.
30. (∃y){Pa • Py • Ra • Ry • ¬ (a = y) • (z)[(Pz • Rz) ⊃ z = a ∨z = y ]} ......... 29 EG m/y
31. (∃x)(∃y){Px • Py • Rx • Ry • ¬ (x = y) • (z)[(Pz • Rz) ⊃ z = x ∨z = y ]} ......... 30 EG a/x