THEOREM

*******

For any set s and binary predicate Q, we have: EXIST(x):[x e s => Q(x,s)]

Prove: ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]

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

PREVIOUS RESULT

***************

Every set must exclude something (from the Paradox of the Universal Set)  Formal Proof

1     ALL(s):[Set(s) => EXIST(a):~a e s]

      Axiom

     PROOF

     *****

     Let s be an arbitrary set

      2     Set(s)

            Premise

     Apply previous result for set s

      3     Set(s) => EXIST(a):~a e s

            U Spec, 1

      4     EXIST(a):~a e s

            Detach, 3, 2

     Introduce x

     Apply Existential Specification Rule

      5     ~x e s

            E Spec, 4

     Introduce arbitrary binary predicate Q(x,s)

     Apply Arbitrary-OR Rule  ('|' is the OR-operator)

      6     ~x e s | Q(x,s)

            Arb Or, 5

     Apply Imply-OR Rule

      7     ~~x e s => Q(x,s)

            Imply-Or, 6

     Remove double negation

      8     x e s => Q(x,s)

            Rem DNeg, 7

Apply Conclusion Rule

As Required:

9     ALL(s):[Set(s) => EXIST(x):[x e s => Q(x,s)]]

      4 Conclusion, 2