THEOREM

*******

  ALL(a):[EXIST(b):P(b) => P(a) <=> ALL(b):[P(b) => P(a)]]

This proof was written and verified with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com

     PROOF

     *****

     '=>'

     Prove: ALL(a):[EXIST(b):P(b) => P(a) => ALL(b):[P(b) => P(a)]]

     Suppose...

      1     EXIST(b):P(b) => P(y)

            Premise

          Prove: ALL(b):[P(b) => P(y)]

          Suppose...

            2     P(x)

                  Premise

            3     EXIST(b):P(b)

                  E Gen, 2

            4     P(y)

                  Detach, 1, 3

     As Required:

      5     ALL(b):[P(b) => P(y)]

            4 Conclusion, 2

As Required:

6     ALL(a):[EXIST(b):P(b) => P(a) => ALL(b):[P(b) => P(a)]]

      4 Conclusion, 1

     '<='

     Prove: ALL(a):[ALL(b):[P(b) => P(a)] => [EXIST(b):P(b) => P(a)]]

     Suppose...

      7     ALL(b):[P(b) => P(y)]

            Premise

          Prove: EXIST(b):P(b) => P(y)

          Suppose...

            8     EXIST(b):P(b)

                  Premise

            9     P(x)

                  E Spec, 8

            10    P(x) => P(y)

                  U Spec, 7

            11    P(y)

                  Detach, 10, 9

     As Required:

      12    EXIST(b):P(b) => P(y)

            4 Conclusion, 8

As Required:

13    ALL(a):[ALL(b):[P(b) => P(a)] => [EXIST(b):P(b) => P(a)]]

      4 Conclusion, 7

Joining results...

14    ALL(a):[[EXIST(b):P(b) => P(a) => ALL(b):[P(b) => P(a)]]

     & [ALL(b):[P(b) => P(a)] => [EXIST(b):P(b) => P(a)]]]

      Join, 6, 13

As Required:

15    ALL(a):[EXIST(b):P(b) => P(a)

     <=> ALL(b):[P(b) => P(a)]]

      Iff-And, 14