Theorem uniun 4891

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 1905	. . . 4 ⊢ (∃𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
2		elun 4109	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))
3	2	anbi2i 634	. . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ (𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)))
4		andi 1023	. . . . . 6 ⊢ ((𝑥 ∈ 𝑦 ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
5	3, 4	bitri 278	. . . . 5 ⊢ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
6	5	exbii 1871	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ ∃𝑦((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
7		eluni 4871	. . . . 5 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴))
8		eluni 4871	. . . . 5 ⊢ (𝑥 ∈ ∪ 𝐵 ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵))
9	7, 8	orbi12i 927	. . . 4 ⊢ ((𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵) ↔ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) ∨ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)))
10	1, 6, 9	3bitr4i 306	. . 3 ⊢ (∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)) ↔ (𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵))
11		eluni 4871	. . 3 ⊢ (𝑥 ∈ ∪ (𝐴 ∪ 𝐵) ↔ ∃𝑦(𝑥 ∈ 𝑦 ∧ 𝑦 ∈ (𝐴 ∪ 𝐵)))
12		elun 4109	. . 3 ⊢ (𝑥 ∈ (∪ 𝐴 ∪ ∪ 𝐵) ↔ (𝑥 ∈ ∪ 𝐴 ∨ 𝑥 ∈ ∪ 𝐵))
13	10, 11, 12	3bitr4i 306	. 2 ⊢ (𝑥 ∈ ∪ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ (∪ 𝐴 ∪ ∪ 𝐵))
14	13	eqriv 2762	1 ⊢ ∪ (𝐴 ∪ 𝐵) = (∪ 𝐴 ∪ ∪ 𝐵)

Syntax hints:   ∧ wa 400   ∨ wo 860   = wceq 1563  ∃wex 1802   ∈ wcel 2145   ∪ cun 3905  ∪ cuni 4868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-uni 4869

This theorem is referenced by:  unidif0  5321  unidif0OLD  5322  unisucs  6429  fvun  6961  onuninsuci  7824  tc2  9697  fin1a2lem10  10381  fin1a2lem12  10383  incexclem  15880  dprd2da  20105  dmdprdsplit2lem  20108  ordtuni  23308  cmpcld  23520  uncmp  23521  refun0  23633  lfinun  23643  1stckgenlem  23671  filconn  24001  ufildr  24049  alexsubALTlem3  24167  cldsubg  24229  icccmplem2  24942  uniioombllem3  25705  madeoldsuc  28036  sxbrsigalem0  34578  fiunelcarsg  34623  carsgclctunlem1  34624  carsggect  34625  tz9.1regs  35442  cvmscld  35636  refssfne  36731  topjoin  36738  ttcuniun  36883  ttcuni  36886  pibt2  37923  mbfresfi  38177  onsucunitp  43962  oaun3  43971  fourierdlem80  46758  isomenndlem  47102