Metamath Proof Explorer


Theorem iununi

Description: A relationship involving union and indexed union. Exercise 25 of Enderton p. 33. (Contributed by NM, 25-Nov-2003) (Proof shortened by Mario Carneiro, 17-Nov-2016)

Ref Expression
Assertion iununi B = A = A B = x B A x

Proof

Step Hyp Ref Expression
1 df-ne B ¬ B =
2 iunconst B x B A = A
3 1 2 sylbir ¬ B = x B A = A
4 iun0 x B =
5 id A = A =
6 5 iuneq2d A = x B A = x B
7 4 6 5 3eqtr4a A = x B A = A
8 3 7 ja B = A = x B A = A
9 8 eqcomd B = A = A = x B A
10 9 uneq1d B = A = A x B x = x B A x B x
11 uniiun B = x B x
12 11 uneq2i A B = A x B x
13 iunun x B A x = x B A x B x
14 10 12 13 3eqtr4g B = A = A B = x B A x
15 unieq B = B =
16 uni0 =
17 15 16 eqtrdi B = B =
18 17 uneq2d B = A B = A
19 un0 A = A
20 18 19 eqtrdi B = A B = A
21 iuneq1 B = x B A x = x A x
22 0iun x A x =
23 21 22 eqtrdi B = x B A x =
24 20 23 eqeq12d B = A B = x B A x A =
25 24 biimpcd A B = x B A x B = A =
26 14 25 impbii B = A = A B = x B A x