Metamath Proof Explorer

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 | ∃ x ∈ X u = x
Assertion unisngl ⊢ X = ⋃ C

Proof

Step Hyp Ref Expression
1 dissnref.c ⊢ C = u | ∃ x ∈ X u = x
2 1 unieqi ⊢ ⋃ C = ⋃ u | ∃ x ∈ X u = x
3 simpl ⊢ y ∈ u ∧ u = x → y ∈ u
4 simpr ⊢ y ∈ u ∧ u = x → u = x
5 3 4 eleqtrd ⊢ y ∈ u ∧ u = x → y ∈ x
6 5 exlimiv ⊢ ∃ u y ∈ u ∧ u = x → y ∈ x
7 eqid ⊢ x = x
8 vsnex ⊢ x ∈ V
9 eleq2 ⊢ u = x → y ∈ u ↔ y ∈ x
10 eqeq1 ⊢ u = x → u = x ↔ x = x
11 9 10 anbi12d ⊢ u = x → y ∈ u ∧ u = x ↔ y ∈ x ∧ x = x
12 8 11 spcev ⊢ y ∈ x ∧ x = x → ∃ u y ∈ u ∧ u = x
13 7 12 mpan2 ⊢ y ∈ x → ∃ u y ∈ u ∧ u = x
14 6 13 impbii ⊢ ∃ u y ∈ u ∧ u = x ↔ y ∈ x
15 velsn ⊢ y ∈ x ↔ y = x
16 equcom ⊢ y = x ↔ x = y
17 14 15 16 3bitri ⊢ ∃ u y ∈ u ∧ u = x ↔ x = y
18 17 rexbii ⊢ ∃ x ∈ X ∃ u y ∈ u ∧ u = x ↔ ∃ x ∈ X x = y
19 r19.42v ⊢ ∃ x ∈ X y ∈ u ∧ u = x ↔ y ∈ u ∧ ∃ x ∈ X u = x
20 19 exbii ⊢ ∃ u ∃ x ∈ X y ∈ u ∧ u = x ↔ ∃ u y ∈ u ∧ ∃ x ∈ X u = x
21 rexcom4 ⊢ ∃ x ∈ X ∃ u y ∈ u ∧ u = x ↔ ∃ u ∃ x ∈ X y ∈ u ∧ u = x
22 eluniab ⊢ y ∈ ⋃ u | ∃ x ∈ X u = x ↔ ∃ u y ∈ u ∧ ∃ x ∈ X u = x
23 20 21 22 3bitr4ri ⊢ y ∈ ⋃ u | ∃ x ∈ X u = x ↔ ∃ x ∈ X ∃ u y ∈ u ∧ u = x
24 risset ⊢ y ∈ X ↔ ∃ x ∈ X x = y
25 18 23 24 3bitr4i ⊢ y ∈ ⋃ u | ∃ x ∈ X u = x ↔ y ∈ X
26 25 eqriv ⊢ ⋃ u | ∃ x ∈ X u = x = X
27 2 26 eqtr2i ⊢ X = ⋃ C