Suppose...

      1     ALL(x):[x e r <=> ~x e x]

            Premise

     Apply Universal Specification for x=r

      2     r e r <=> ~r e r

            U Spec, 1

      3     [r e r => ~r e r] & [~r e r => r e r]

            Iff-And, 2

      4     r e r => ~r e r

            Split, 3

      5     ~r e r => r e r

            Split, 3

          Suppose...

            6     r e r

                  Premise

            7     ~r e r

                  Detach, 4, 6

            8     r e r & ~r e r

                  Join, 6, 7

     By contradiction...

      9     ~r e r

            4 Conclusion, 6

Generalizing...

10    ALL(r):[ALL(x):[x e r <=> ~x e x] => ~r e r]

      4 Conclusion, 1