Theorem

-------

The empty set is unique. All empty sets are identical.

ALL(e1):ALL(e2):[Set(e1) & Set(e2)

=> [~EXIST(a):a e e1 & ~EXIST(a):a e e2 => e1=e2]]

By Dan Christensen

Proof

-----

Suppose...

1     Set(e1) & Set(e2)

Premise

Splitting this premise...

2     Set(e1)

Split, 1

3     Set(e2)

Split, 1

Prove: ~EXIST(a):a e e1 & ~EXIST(a):a e e2 => e1=e2

Suppose...

4     ~EXIST(a):a e e1 & ~EXIST(a):a e e2

Premise

5     ~EXIST(a):a e e1

Split, 4

6     ~EXIST(a):a e e2

Split, 4

Apply Set Equality Axiom

7     ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]

Set Equality

8     ALL(b):[Set(e1) & Set(b) => [e1=b <=> ALL(c):[c e e1 <=> c e b]]]

U Spec, 7

9     Set(e1) & Set(e2) => [e1=e2 <=> ALL(c):[c e e1 <=> c e e2]]

U Spec, 8

10    e1=e2 <=> ALL(c):[c e e1 <=> c e e2]

Detach, 9, 1

11    [e1=e2 => ALL(c):[c e e1 <=> c e e2]]

& [ALL(c):[c e e1 <=> c e e2] => e1=e2]

Iff-And, 10

12    e1=e2 => ALL(c):[c e e1 <=> c e e2]

Split, 11

Sufficient: For e1=e2

13    ALL(c):[c e e1 <=> c e e2] => e1=e2

Split, 11

Switch quantifiers and remove ~~

14    ~~ALL(a):~a e e1

Quant, 5

15    ALL(a):~a e e1

Rem DNeg, 14

16    ~~ALL(a):~a e e2

Quant, 6

17    ALL(a):~a e e2

Rem DNeg, 16

Prove: ALL(a):[~a e e2 => ~a e e1]  (contrapositive)

18    ~x e e2

Premise

19    ~x e e1

U Spec, 15

As Required:

20    ALL(a):[~a e e2 => ~a e e1]

4 Conclusion, 18

Apply Contrapositive Rule and remove ~~

21    ALL(a):[~~a e e1 => ~~a e e2]

Contra, 20

22    ALL(a):[a e e1 => ~~a e e2]

Rem DNeg, 21

'=>'

As Required:

23    ALL(a):[a e e1 => a e e2]

Rem DNeg, 22

Prove: ALL(a):[~a e e1 => ~a e e2]  (contrapositive)

Suppose...

24    ~x e e1

Premise

25    ~x e e2

U Spec, 17

As Required:

26    ALL(a):[~a e e1 => ~a e e2]

4 Conclusion, 24

Apply the Contrapositive Rule and remove ~~

27    ALL(a):[~~a e e2 => ~~a e e1]

Contra, 26

28    ALL(a):[a e e2 => ~~a e e1]

Rem DNeg, 27

'<='

As Required:

29    ALL(a):[a e e2 => a e e1]

Rem DNeg, 28

Apply Join Rule using single quantifier option

30    ALL(a):[[a e e1 => a e e2] & [a e e2 => a e e1]]

Join, 23, 29

31    ALL(a):[a e e1 <=> a e e2]

Iff-And, 30

32    e1=e2

Detach, 13, 31

As Required:

33    ~EXIST(a):a e e1 & ~EXIST(a):a e e2 => e1=e2

4 Conclusion, 4

As Required:

34    ALL(e1):ALL(e2):[Set(e1) & Set(e2)

=> [~EXIST(a):a e e1 & ~EXIST(a):a e e2 => e1=e2]]

4 Conclusion, 1