The Logic Book, M. Bergmann, J. Moor, J. Nelson, McGraw Hill, 2004, 10.4E, 1(a), p. 553

We have to derive: (x)Ax ≡ (x)(Ax • Ax). We start by making an assumption:

1. * (x)Ax ......... ACP
2. * Ax ......... 1 UI
3. * Ax ......... 2 Rep.
4. * Ax • Ax ......... 2,3 Conj.
5. * (x)(Ax • Ax) ......... 4 UG
6. (x)Ax ⊃(x)(Ax • Ax) ......... 1-5 CP
7. * (x)(Ax • Ax) ......... ACP
8. * Ax • Ax ......... 7 UI
9. * Ax ......... Simp.
10. * (x)Ax ......... 9 UG
11. (x)(Ax • Ax) ⊃(x)Ax ......... 7-10 CP
12. [(x)Ax ⊃(x)(Ax • Ax)] • [(x)(Ax • Ax) ⊃(x)Ax] ......... 6,11 Conj.
13. (x)Ax ≡ (x)(Ax • Ax) ......... 12 BE