Theorem unisngl

Description: Taking the union of the set of singletons recovers the initial set. (Contributed by Thierry Arnoux, 9-Jan-2020)

	Ref	Expression
Hypothesis	dissnref.c	|- C = { u | E. x e. X u = { x } }
Assertion	unisngl	|- X = U. C

Proof

Step	Hyp	Ref	Expression
1		dissnref.c	|- C = { u | E. x e. X u = { x } }
2	1	unieqi	|- U. C = U. { u | E. x e. X u = { x } }
3		simpl	|- ( ( y e. u /\ u = { x } ) -> y e. u )
4		simpr	|- ( ( y e. u /\ u = { x } ) -> u = { x } )
5	3 4	eleqtrd	|- ( ( y e. u /\ u = { x } ) -> y e. { x } )
6	5	exlimiv	|- ( E. u ( y e. u /\ u = { x } ) -> y e. { x } )
7		eqid	|- { x } = { x }
8		snex	|- { x } e. _V
9		eleq2	|- ( u = { x } -> ( y e. u <-> y e. { x } ) )
10		eqeq1	|- ( u = { x } -> ( u = { x } <-> { x } = { x } ) )
11	9 10	anbi12d	|- ( u = { x } -> ( ( y e. u /\ u = { x } ) <-> ( y e. { x } /\ { x } = { x } ) ) )
12	8 11	spcev	|- ( ( y e. { x } /\ { x } = { x } ) -> E. u ( y e. u /\ u = { x } ) )
13	7 12	mpan2	|- ( y e. { x } -> E. u ( y e. u /\ u = { x } ) )
14	6 13	impbii	|- ( E. u ( y e. u /\ u = { x } ) <-> y e. { x } )
15		velsn	|- ( y e. { x } <-> y = x )
16		equcom	|- ( y = x <-> x = y )
17	14 15 16	3bitri	|- ( E. u ( y e. u /\ u = { x } ) <-> x = y )
18	17	rexbii	|- ( E. x e. X E. u ( y e. u /\ u = { x } ) <-> E. x e. X x = y )
19		r19.42v	|- ( E. x e. X ( y e. u /\ u = { x } ) <-> ( y e. u /\ E. x e. X u = { x } ) )
20	19	exbii	|- ( E. u E. x e. X ( y e. u /\ u = { x } ) <-> E. u ( y e. u /\ E. x e. X u = { x } ) )
21		rexcom4	|- ( E. x e. X E. u ( y e. u /\ u = { x } ) <-> E. u E. x e. X ( y e. u /\ u = { x } ) )
22		eluniab	|- ( y e. U. { u | E. x e. X u = { x } } <-> E. u ( y e. u /\ E. x e. X u = { x } ) )
23	20 21 22	3bitr4ri	|- ( y e. U. { u | E. x e. X u = { x } } <-> E. x e. X E. u ( y e. u /\ u = { x } ) )
24		risset	|- ( y e. X <-> E. x e. X x = y )
25	18 23 24	3bitr4i	|- ( y e. U. { u | E. x e. X u = { x } } <-> y e. X )
26	25	eqriv	|- U. { u | E. x e. X u = { x } } = X
27	2 26	eqtr2i	|- X = U. C