Response to Naive Set Theory Question (sci.math)

Theorem: If setA is a non-empty set, and setx is the singleton containing only x,
and setA is contained in (i.e. a subset of) setx, then setA=setx

Outline:

Show p ε setA <=> p ε setx

'=>'  

Suppose p ε setA. Since setA is contained in setx, we have p ε setx.   

'<='

Now, suppose p ε setx. By the definition of setx, we have p=x. Let q ε setA. Since 
setA is contained in setx, we have q ε setx. By the definition of setx, we have q=x. 
Substituting, we have p=q and p ε setA.


Formal Proof:

Suppose setA is a non-empty set, 
and setx is the singleton containing only x,
and setA is contained in setx.

1	Set(setA)
	& EXIST(a):a ε setA
	& Set(setx)
	& ALL(a):[a ε setx <=> a=x]
	& ALL(a):[a ε setA => a ε setx]
	Premise

2	Set(setA)
	Split, 1

3	EXIST(a):a ε setA
	Split, 1

4	Set(setx)
	Split, 1

5	ALL(a):[a ε setx <=> a=x]
	Split, 1

6	ALL(a):[a ε setA => a ε setx]
	Split, 1

Applying set axiom...

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

8	ALL(b):[Set(setA) & Set(b) => [setA=b <=> ALL(c):[c ε setA <=> c ε b]]]
	U Spec, 7

9	Set(setA) & Set(setx) => [setA=setx <=> ALL(c):[c ε setA <=> c ε setx]]
	U Spec, 8

10	Set(setA) & Set(setx)
	Join, 2, 4

11	setA=setx <=> ALL(c):[c ε setA <=> c ε setx]
	Detach, 9, 10

12	[setA=setx => ALL(c):[c ε setA <=> c ε setx]]
	& [ALL(c):[c ε setA <=> c ε setx] => setA=setx]
	Iff-And, 11

13	setA=setx => ALL(c):[c ε setA <=> c ε setx]
	Split, 12

Sufficient: For setA=setx

14	ALL(c):[c ε setA <=> c ε setx] => setA=setx
	Split, 12

	
	'=>'
	
	Prove: p ε setA => p ε setx
	
	Suppose...

	15	p ε setA
		Premise

	Applying definition of setx...

	16	p ε setx <=> p=x
		U Spec, 5

	17	[p ε setx => p=x] & [p=x => p ε setx]
		Iff-And, 16

	18	p ε setx => p=x
		Split, 17

	Sufficient: For p ε setx

	19	p=x => p ε setx
		Split, 17

	Since setA is contained in setx...

	20	p ε setA => p ε setx
		U Spec, 6

	21	p ε setx
		Detach, 20, 15

'=>'

As Required:

22	p ε setA => p ε setx
	Conclusion, 15
	
	'<='
	
	Prove: p ε setx => p ε setA
	
	Suppose...

	23	p ε setx
		Premise

	Applying definition of setx...

	24	p ε setx <=> p=x
		U Spec, 5

	25	[p ε setx => p=x] & [p=x => p ε setx]
		Iff-And, 24

	26	p ε setx => p=x
		Split, 25

	27	p=x => p ε setx
		Split, 25

	28	p=x
		Detach, 26, 23

	Let q be such that...

	29	q ε setA
		E Spec, 3

	Since setA is contained in setx...

	30	q ε setA => q ε setx
		U Spec, 6

	31	q ε setx
		Detach, 30, 29

	Applying the definition of setx...

	32	q ε setx <=> q=x
		U Spec, 5

	33	[q ε setx => q=x] & [q=x => q ε setx]
		Iff-And, 32

	34	q ε setx => q=x
		Split, 33

	35	q=x => q ε setx
		Split, 33

	36	q=x
		Detach, 34, 31

	Substituting...

	37	p=q
		Substitute, 36, 28

	38	p ε setA
		Substitute, 37, 29

As Required:

39	p ε setx => p ε setA
	Conclusion, 23
Combining results...

40	[p ε setA => p ε setx] & [p ε setx => p ε setA]
	Join, 22, 39

41	p ε setA <=> p ε setx
	Iff-And, 40

Generalizing...

42	ALL(c):[c ε setA <=> c ε setx]
	U Gen, 41

As Required:

43	setA=setx
	Detach, 14, 42