Theorem iunxiun 4049

Description: Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016.)

Assertion

Ref	Expression
iunxiun	⊢ ∪x ∈ ∪ y ∈ A BC = ∪y ∈ A ∪x ∈ B C

Distinct variable groups:   x,y   x,A   y,C

Allowed substitution hints:   A(y)   B(x,y)   C(x)

Proof of Theorem iunxiun

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eliun 3974	. . . . . . . 8 ⊢ (x ∈ ∪y ∈ A B ↔ ∃y ∈ A x ∈ B)
2	1	anbi1i 676	. . . . . . 7 ⊢ ((x ∈ ∪y ∈ A B ∧ z ∈ C) ↔ (∃y ∈ A x ∈ B ∧ z ∈ C))
3		r19.41v 2765	. . . . . . 7 ⊢ (∃y ∈ A (x ∈ B ∧ z ∈ C) ↔ (∃y ∈ A x ∈ B ∧ z ∈ C))
4	2, 3	bitr4i 243	. . . . . 6 ⊢ ((x ∈ ∪y ∈ A B ∧ z ∈ C) ↔ ∃y ∈ A (x ∈ B ∧ z ∈ C))
5	4	exbii 1582	. . . . 5 ⊢ (∃x(x ∈ ∪y ∈ A B ∧ z ∈ C) ↔ ∃x∃y ∈ A (x ∈ B ∧ z ∈ C))
6		rexcom4 2879	. . . . 5 ⊢ (∃y ∈ A ∃x(x ∈ B ∧ z ∈ C) ↔ ∃x∃y ∈ A (x ∈ B ∧ z ∈ C))
7	5, 6	bitr4i 243	. . . 4 ⊢ (∃x(x ∈ ∪y ∈ A B ∧ z ∈ C) ↔ ∃y ∈ A ∃x(x ∈ B ∧ z ∈ C))
8		df-rex 2621	. . . 4 ⊢ (∃x ∈ ∪ y ∈ A Bz ∈ C ↔ ∃x(x ∈ ∪y ∈ A B ∧ z ∈ C))
9		eliun 3974	. . . . . 6 ⊢ (z ∈ ∪x ∈ B C ↔ ∃x ∈ B z ∈ C)
10		df-rex 2621	. . . . . 6 ⊢ (∃x ∈ B z ∈ C ↔ ∃x(x ∈ B ∧ z ∈ C))
11	9, 10	bitri 240	. . . . 5 ⊢ (z ∈ ∪x ∈ B C ↔ ∃x(x ∈ B ∧ z ∈ C))
12	11	rexbii 2640	. . . 4 ⊢ (∃y ∈ A z ∈ ∪x ∈ B C ↔ ∃y ∈ A ∃x(x ∈ B ∧ z ∈ C))
13	7, 8, 12	3bitr4i 268	. . 3 ⊢ (∃x ∈ ∪ y ∈ A Bz ∈ C ↔ ∃y ∈ A z ∈ ∪x ∈ B C)
14		eliun 3974	. . 3 ⊢ (z ∈ ∪x ∈ ∪ y ∈ A BC ↔ ∃x ∈ ∪ y ∈ A Bz ∈ C)
15		eliun 3974	. . 3 ⊢ (z ∈ ∪y ∈ A ∪x ∈ B C ↔ ∃y ∈ A z ∈ ∪x ∈ B C)
16	13, 14, 15	3bitr4i 268	. 2 ⊢ (z ∈ ∪x ∈ ∪ y ∈ A BC ↔ z ∈ ∪y ∈ A ∪x ∈ B C)
17	16	eqriv 2350	1 ⊢ ∪x ∈ ∪ y ∈ A BC = ∪y ∈ A ∪x ∈ B C

Syntax hints:   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  ∃wrex 2616  ∪ciun 3970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ral 2620  df-rex 2621  df-v 2862  df-iun 3972

This theorem is referenced by: (None)