Theorem uniun 4887

Description: The class union of the union of two classes. Theorem 8.3 of [Quine] p. 53. (Contributed by NM, 20-Aug-1993.)

Assertion

Ref	Expression
uniun	⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵)

Proof of Theorem uniun

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		19.43 1901	. . . 4 ⊢ (∃𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
2		elun 4106	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))
3	2	anbi2i 632	. . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ (𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)))
4		andi 1020	. . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
5	3, 4	bitri 277	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
6	5	exbii 1867	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ ∃𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
7		eluni 4867	. . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
8		eluni 4867	. . . . 5 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
9	7, 8	orbi12i 925	. . . 4 ⊢ ((𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
10	1, 6, 9	3bitr4i 305	. . 3 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ (𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵))
11		eluni 4867	. . 3 ⊢ (𝑥 ∈ ∪ (𝐴 ∪ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)))
12		elun 4106	. . 3 ⊢ (𝑥 ∈ (∪ 𝐴 ∪ ∪ 𝐵) ↔ (𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵))
13	10, 11, 12	3bitr4i 305	. 2 ⊢ (𝑥 ∈ ∪ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ (∪ 𝐴 ∪ ∪ 𝐵))
14	13	eqriv 2758	1 ⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵)

Syntax hints:   ∧ wa 399   ∨ wo 858   = wceq 1559  ∃wex 1798   ∈ wcel 2141   ∪ cun 3902  ∪ cuni 4864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-uni 4865

This theorem is referenced by:  unidif0  5315  unidif0OLD  5316  unisucs  6421  fvun  6953  onuninsuci  7816  tc2  9692  fin1a2lem10  10363  fin1a2lem12  10365  incexclem  15849  dprd2da  20067  dmdprdsplit2lem  20070  ordtuni  23230  cmpcld  23442  uncmp  23443  refun0  23555  lfinun  23565  1stckgenlem  23593  filconn  23923  ufildr  23971  alexsubALTlem3  24089  cldsubg  24151  icccmplem2  24864  uniioombllem3  25627  madeoldsuc  27955  sxbrsigalem0  34529  fiunelcarsg  34574  carsgclctunlem1  34575  carsggect  34576  tz9.1regs  35394  cvmscld  35587  refssfne  36682  topjoin  36689  ttcuniun  36834  ttcuni  36837  pibt2  37875  mbfresfi  38129  onsucunitp  43914  oaun3  43923  fourierdlem80  46724  isomenndlem  47068