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 |
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 |