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