Theorem dmsnsnsn

Description: The domain of the singleton of the singleton of a singleton. (Contributed by NM, 15-Sep-2004) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	dmsnsnsn	|- dom { { { A } } } = { A }

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	opid	|- <. x , x >. = { { x } }
3		sneq	|- ( x = A -> { x } = { A } )
4	3	sneqd	|- ( x = A -> { { x } } = { { A } } )
5	2 4	syl5eq	|- ( x = A -> <. x , x >. = { { A } } )
6	5	sneqd	|- ( x = A -> { <. x , x >. } = { { { A } } } )
7	6	dmeqd	|- ( x = A -> dom { <. x , x >. } = dom { { { A } } } )
8	7 3	eqeq12d	|- ( x = A -> ( dom { <. x , x >. } = { x } <-> dom { { { A } } } = { A } ) )
9	1	dmsnop	|- dom { <. x , x >. } = { x }
10	8 9	vtoclg	|- ( A e. _V -> dom { { { A } } } = { A } )
11		0ex	|- (/) e. _V
12	11	snid	|- (/) e. { (/) }
13		dmsn0el	|- ( (/) e. { (/) } -> dom { { (/) } } = (/) )
14	12 13	ax-mp	|- dom { { (/) } } = (/)
15		snprc	|- ( -. A e. _V <-> { A } = (/) )
16	15	biimpi	|- ( -. A e. _V -> { A } = (/) )
17	16	sneqd	|- ( -. A e. _V -> { { A } } = { (/) } )
18	17	sneqd	|- ( -. A e. _V -> { { { A } } } = { { (/) } } )
19	18	dmeqd	|- ( -. A e. _V -> dom { { { A } } } = dom { { (/) } } )
20	14 19 16	3eqtr4a	|- ( -. A e. _V -> dom { { { A } } } = { A } )
21	10 20	pm2.61i	|- dom { { { A } } } = { A }