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
|- U_ x e. A { x } = A

Proof

Step Hyp Ref Expression
1 df-iun
 |-  U_ x e. A { x } = { y | E. x e. A y e. { x } }
2 clel5
 |-  ( y e. A <-> E. x e. A y = x )
3 velsn
 |-  ( y e. { x } <-> y = x )
4 3 rexbii
 |-  ( E. x e. A y e. { x } <-> E. x e. A y = x )
5 2 4 bitr4i
 |-  ( y e. A <-> E. x e. A y e. { x } )
6 5 eqabi
 |-  A = { y | E. x e. A y e. { x } }
7 1 6 eqtr4i
 |-  U_ x e. A { x } = A