Description: An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005) (Proof shortened by SN, 15-Jan-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | iunid | ⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iun | ⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑥 } } | |
2 | clel5 | ⊢ ( 𝑦 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝑥 ) | |
3 | velsn | ⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 ) | |
4 | 3 | rexbii | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑥 } ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝑥 ) |
5 | 2 4 | bitr4i | ⊢ ( 𝑦 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑥 } ) |
6 | 5 | eqabi | ⊢ 𝐴 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑥 } } |
7 | 1 6 | eqtr4i | ⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴 |