Let x = {{}} 
Let y be the set of all elements of x not equal to {}. 
Is the following statement true? 
Az(zey -> zex)

Yes.


Let x be a set such aεx iff a is an empty set.

1	Set(x) & ALL(a):[a ε x <=> Set(a) & ALL(b):~b ε a]
	Premise

2	Set(x)
	Split, 1

3	ALL(a):[a ε x <=> Set(a) & ALL(b):~b ε a]
	Split, 1

Let y be the subset of x, all elements of which are not empty sets.

4	Set(y) & ALL(a):[a ε y <=> a ε x & ~ALL(b):~b ε a]
	Premise

5	Set(y)
	Split, 4

6	ALL(a):[a ε y <=> a ε x & ~ALL(b):~b ε a]
	Split, 4

	
	Prove: For arbitrary p, ~pεy
	
	Suppose to the contrary...

	7	p ε y
		Premise

	Applying the definition of y...

	8	p ε y <=> p ε x & ~ALL(b):~b ε p
		U Spec, 6

	9	[p ε y => p ε x & ~ALL(b):~b ε p]
		& [p ε x & ~ALL(b):~b ε p => p ε y]
		Iff-And, 8

	10	p ε y => p ε x & ~ALL(b):~b ε p
		Split, 9

	11	p ε x & ~ALL(b):~b ε p => p ε y
		Split, 9

	12	p ε x & ~ALL(b):~b ε p
		Detach, 10, 7

	From the definition of y, we have...

	13	p ε x
		Split, 12

	14	~ALL(b):~b ε p
		Split, 12

	Applying the defintion of x...

	15	p ε x <=> Set(p) & ALL(b):~b ε p
		U Spec, 3

	16	[p ε x => Set(p) & ALL(b):~b ε p]
		& [Set(p) & ALL(b):~b ε p => p ε x]
		Iff-And, 15

	17	p ε x => Set(p) & ALL(b):~b ε p
		Split, 16

	18	Set(p) & ALL(b):~b ε p => p ε x
		Split, 16

	19	Set(p) & ALL(b):~b ε p
		Detach, 17, 13

	From the definition of x, we have...

	20	Set(p)
		Split, 19

	21	ALL(b):~b ε p
		Split, 19

	We obtain the contradiction...

	22	~ALL(b):~b ε p & ALL(b):~b ε p
		Join, 14, 21

As required...

23	~p ε y
	Conclusion, 7

Generalizing, y is an empty set

24	ALL(a):~a ε y
	U Gen, 23

Prove: y is a subset of x

Since y is an empty set, for arbitrary z, we have...

25	~z ε y
	U Spec, 24

26	~z ε x => ~z ε y
	Arb Ante, 25

27	~~z ε y => ~~z ε x
	Contra, 26

28	z ε y => ~~z ε x
	Rem DNeg, 27

29	z ε y => z ε x
	Rem DNeg, 28

As Required: y is a subset of x

30	ALL(a):[a ε y => a ε x]
	U Gen, 29