MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uniun Structured version   Visualization version   GIF version

Theorem uniun 4930
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.
StepHypRef Expression
1 19.43 1882 . . . 4 (∃𝑦((𝑥𝑦𝑦𝐴) ∨ (𝑥𝑦𝑦𝐵)) ↔ (∃𝑦(𝑥𝑦𝑦𝐴) ∨ ∃𝑦(𝑥𝑦𝑦𝐵)))
2 elun 4153 . . . . . . 7 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴𝑦𝐵))
32anbi2i 623 . . . . . 6 ((𝑥𝑦𝑦 ∈ (𝐴𝐵)) ↔ (𝑥𝑦 ∧ (𝑦𝐴𝑦𝐵)))
4 andi 1010 . . . . . 6 ((𝑥𝑦 ∧ (𝑦𝐴𝑦𝐵)) ↔ ((𝑥𝑦𝑦𝐴) ∨ (𝑥𝑦𝑦𝐵)))
53, 4bitri 275 . . . . 5 ((𝑥𝑦𝑦 ∈ (𝐴𝐵)) ↔ ((𝑥𝑦𝑦𝐴) ∨ (𝑥𝑦𝑦𝐵)))
65exbii 1848 . . . 4 (∃𝑦(𝑥𝑦𝑦 ∈ (𝐴𝐵)) ↔ ∃𝑦((𝑥𝑦𝑦𝐴) ∨ (𝑥𝑦𝑦𝐵)))
7 eluni 4910 . . . . 5 (𝑥 𝐴 ↔ ∃𝑦(𝑥𝑦𝑦𝐴))
8 eluni 4910 . . . . 5 (𝑥 𝐵 ↔ ∃𝑦(𝑥𝑦𝑦𝐵))
97, 8orbi12i 915 . . . 4 ((𝑥 𝐴𝑥 𝐵) ↔ (∃𝑦(𝑥𝑦𝑦𝐴) ∨ ∃𝑦(𝑥𝑦𝑦𝐵)))
101, 6, 93bitr4i 303 . . 3 (∃𝑦(𝑥𝑦𝑦 ∈ (𝐴𝐵)) ↔ (𝑥 𝐴𝑥 𝐵))
11 eluni 4910 . . 3 (𝑥 (𝐴𝐵) ↔ ∃𝑦(𝑥𝑦𝑦 ∈ (𝐴𝐵)))
12 elun 4153 . . 3 (𝑥 ∈ ( 𝐴 𝐵) ↔ (𝑥 𝐴𝑥 𝐵))
1310, 11, 123bitr4i 303 . 2 (𝑥 (𝐴𝐵) ↔ 𝑥 ∈ ( 𝐴 𝐵))
1413eqriv 2734 1 (𝐴𝐵) = ( 𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 395  wo 848   = wceq 1540  wex 1779  wcel 2108  cun 3949   cuni 4907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-uni 4908
This theorem is referenced by:  unidif0  5360  unisucs  6461  fvssunirnOLD  6940  fvun  6999  onuninsuci  7861  tc2  9782  fin1a2lem10  10449  fin1a2lem12  10451  incexclem  15872  dprd2da  20062  dmdprdsplit2lem  20065  ordtuni  23198  cmpcld  23410  uncmp  23411  refun0  23523  lfinun  23533  1stckgenlem  23561  filconn  23891  ufildr  23939  alexsubALTlem3  24057  cldsubg  24119  icccmplem2  24845  uniioombllem3  25620  madeoldsuc  27923  zs12bday  28424  sxbrsigalem0  34273  fiunelcarsg  34318  carsgclctunlem1  34319  carsggect  34320  cvmscld  35278  refssfne  36359  topjoin  36366  pibt2  37418  mbfresfi  37673  onsucunitp  43386  oaun3  43395  fourierdlem80  46201  isomenndlem  46545
  Copyright terms: Public domain W3C validator