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 x A x = A

Proof

Step Hyp Ref Expression
1 df-iun x A x = y | x A y x
2 clel5 y A x A y = x
3 velsn y x y = x
4 3 rexbii x A y x x A y = x
5 2 4 bitr4i y A x A y x
6 5 eqabi A = y | x A y x
7 1 6 eqtr4i x A x = A