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

Theorem uniun 4591
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 1961 . . . 4 (∃𝑦((𝑥𝑦𝑦𝐴) ∨ (𝑥𝑦𝑦𝐵)) ↔ (∃𝑦(𝑥𝑦𝑦𝐴) ∨ ∃𝑦(𝑥𝑦𝑦𝐵)))
2 elun 3902 . . . . . . 7 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴𝑦𝐵))
32anbi2i 601 . . . . . 6 ((𝑥𝑦𝑦 ∈ (𝐴𝐵)) ↔ (𝑥𝑦 ∧ (𝑦𝐴𝑦𝐵)))
4 andi 967 . . . . . 6 ((𝑥𝑦 ∧ (𝑦𝐴𝑦𝐵)) ↔ ((𝑥𝑦𝑦𝐴) ∨ (𝑥𝑦𝑦𝐵)))
53, 4bitri 264 . . . . 5 ((𝑥𝑦𝑦 ∈ (𝐴𝐵)) ↔ ((𝑥𝑦𝑦𝐴) ∨ (𝑥𝑦𝑦𝐵)))
65exbii 1923 . . . 4 (∃𝑦(𝑥𝑦𝑦 ∈ (𝐴𝐵)) ↔ ∃𝑦((𝑥𝑦𝑦𝐴) ∨ (𝑥𝑦𝑦𝐵)))
7 eluni 4575 . . . . 5 (𝑥 𝐴 ↔ ∃𝑦(𝑥𝑦𝑦𝐴))
8 eluni 4575 . . . . 5 (𝑥 𝐵 ↔ ∃𝑦(𝑥𝑦𝑦𝐵))
97, 8orbi12i 879 . . . 4 ((𝑥 𝐴𝑥 𝐵) ↔ (∃𝑦(𝑥𝑦𝑦𝐴) ∨ ∃𝑦(𝑥𝑦𝑦𝐵)))
101, 6, 93bitr4i 292 . . 3 (∃𝑦(𝑥𝑦𝑦 ∈ (𝐴𝐵)) ↔ (𝑥 𝐴𝑥 𝐵))
11 eluni 4575 . . 3 (𝑥 (𝐴𝐵) ↔ ∃𝑦(𝑥𝑦𝑦 ∈ (𝐴𝐵)))
12 elun 3902 . . 3 (𝑥 ∈ ( 𝐴 𝐵) ↔ (𝑥 𝐴𝑥 𝐵))
1310, 11, 123bitr4i 292 . 2 (𝑥 (𝐴𝐵) ↔ 𝑥 ∈ ( 𝐴 𝐵))
1413eqriv 2767 1 (𝐴𝐵) = ( 𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 382  wo 826   = wceq 1630  wex 1851  wcel 2144  cun 3719   cuni 4572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-un 3726  df-uni 4573
This theorem is referenced by:  unidif0  4966  unisuc  5944  fvssunirn  6358  fvun  6410  onuninsuci  7186  tc2  8781  fin1a2lem10  9432  fin1a2lem12  9434  incexclem  14774  dprd2da  18648  dmdprdsplit2lem  18651  ordtuni  21214  cmpcld  21425  uncmp  21426  refun0  21538  lfinun  21548  1stckgenlem  21576  filconn  21906  ufildr  21954  alexsubALTlem3  22072  cldsubg  22133  icccmplem2  22845  uniioombllem3  23572  sxbrsigalem0  30667  fiunelcarsg  30712  carsgclctunlem1  30713  carsggect  30714  cvmscld  31587  noetalem4  32197  refssfne  32684  topjoin  32691  mbfresfi  33781  fourierdlem80  40914  isomenndlem  41258
  Copyright terms: Public domain W3C validator