Metamath Proof Explorer


Theorem iunid

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 𝑥𝐴 { 𝑥 } = 𝐴

Proof

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 𝑥𝐴 { 𝑥 } = 𝐴