The Logic Book, M. Bergmann, J. Moor, J. Nelson, McGraw Hill, 2004, 10.4E, 5(f), p. 557

We are asked to show that sentences in this pair are equivalent:

1. (x)(y)[(Axy • Ayx) ⊃ Axx]
2. (x)[(∃y)(Axy • Ayx) ⊃ Axx]

The proof:

1. (x)(y)[(Axy • Ayx) ⊃ Axx]
2. * (∃y)(Axy • Ayx) ......... ACP
3. * Axm • Amx ......... 2 EI y/m
4. * (y)[(Axy • Ayx) ⊃ Axx] ......... 1 UI x/x
5. * (Axm • Amx) ⊃ Axx ......... 4 UI y/m
6. * Axx ......... 3,5 MP
7. (∃y)(Axy • Ayx) ⊃ Axx ......... 2-6 CP
8. (x)[(∃y)(Axy • Ayx) ⊃ Axx] ......... 7 UG

and in reverse:

1. (x)[(∃y)(Axy • Ayx) ⊃ Axx]
2. * Axy • Ayx ......... ACP
3. * (∃y)(Axy • Ayx) ......... 2 EG
4. * (∃y)(Axy • Ayx) ⊃ Axx ......... 1 UI x/x
5. * Axx ......... 3,4 MP
6. (Axy • Ayx) ⊃ Axx ......... 2-5 CP
7. (y)[(Axy • Ayx) ⊃Axx] ......... 6 UG
8. (x)(y)[(Axy • Ayx) ⊃Axx] ......... 7 UG