"Frege's" proof: (1) | ~Ax~AyRxy A (2) | | Ax~Rxb A (3) | | ~Rab 2 AE (4) | | | AyRay A (5) | | | Rab 4 AE (6) | | ~AyRay 4,3,5 RAA (7) | | Ax~AyRxy 6 AI (8) | ~Ax~Rxb 2,1,7 RAA (9) | Ay~Ax~Rxy 8 AI (10) ~Ax~AyRxy -> Ay~Ax~Rxy 1,9 ->I Dan's version: 1 ~ALL(x):~ALL(y):R(x,y) Premise 2 ALL(x):~R(x,b) Premise 3 ~R(a,b) U Spec, 2 4 ALL(y):R(a,y) Premise 5 R(a,b) U Spec, 4 6 R(a,b) & ~R(a,b) Join, 5, 3 7 ~ALL(y):R(a,y) Conclusion, 4 8 ALL(x):~ALL(y):R(x,y) U Gen, 7 9 ALL(x):~ALL(y):R(x,y) & ~ALL(x):~ALL(y):R(x,y) Join, 8, 1 10 ~ALL(x):~R(x,b) Conclusion, 2 11 ALL(y):~ALL(x):~R(x,y) U Gen, 10 12 ~ALL(x):~ALL(y):R(x,y) => ALL(y):~ALL(x):~R(x,y) Conclusion, 1