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 |