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