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

Theorem uniun 4217
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  |-  U. ( A  u.  B )  =  ( U. A  u.  U. B )

Proof of Theorem uniun
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 19.43 1745 . . . 4  |-  ( E. y ( ( x  e.  y  /\  y  e.  A )  \/  (
x  e.  y  /\  y  e.  B )
)  <->  ( E. y
( x  e.  y  /\  y  e.  A
)  \/  E. y
( x  e.  y  /\  y  e.  B
) ) )
2 elun 3574 . . . . . . 7  |-  ( y  e.  ( A  u.  B )  <->  ( y  e.  A  \/  y  e.  B ) )
32anbi2i 700 . . . . . 6  |-  ( ( x  e.  y  /\  y  e.  ( A  u.  B ) )  <->  ( x  e.  y  /\  (
y  e.  A  \/  y  e.  B )
) )
4 andi 878 . . . . . 6  |-  ( ( x  e.  y  /\  ( y  e.  A  \/  y  e.  B
) )  <->  ( (
x  e.  y  /\  y  e.  A )  \/  ( x  e.  y  /\  y  e.  B
) ) )
53, 4bitri 253 . . . . 5  |-  ( ( x  e.  y  /\  y  e.  ( A  u.  B ) )  <->  ( (
x  e.  y  /\  y  e.  A )  \/  ( x  e.  y  /\  y  e.  B
) ) )
65exbii 1718 . . . 4  |-  ( E. y ( x  e.  y  /\  y  e.  ( A  u.  B
) )  <->  E. y
( ( x  e.  y  /\  y  e.  A )  \/  (
x  e.  y  /\  y  e.  B )
) )
7 eluni 4201 . . . . 5  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
8 eluni 4201 . . . . 5  |-  ( x  e.  U. B  <->  E. y
( x  e.  y  /\  y  e.  B
) )
97, 8orbi12i 524 . . . 4  |-  ( ( x  e.  U. A  \/  x  e.  U. B
)  <->  ( E. y
( x  e.  y  /\  y  e.  A
)  \/  E. y
( x  e.  y  /\  y  e.  B
) ) )
101, 6, 93bitr4i 281 . . 3  |-  ( E. y ( x  e.  y  /\  y  e.  ( A  u.  B
) )  <->  ( x  e.  U. A  \/  x  e.  U. B ) )
11 eluni 4201 . . 3  |-  ( x  e.  U. ( A  u.  B )  <->  E. y
( x  e.  y  /\  y  e.  ( A  u.  B ) ) )
12 elun 3574 . . 3  |-  ( x  e.  ( U. A  u.  U. B )  <->  ( x  e.  U. A  \/  x  e.  U. B ) )
1310, 11, 123bitr4i 281 . 2  |-  ( x  e.  U. ( A  u.  B )  <->  x  e.  ( U. A  u.  U. B ) )
1413eqriv 2448 1  |-  U. ( A  u.  B )  =  ( U. A  u.  U. B )
Colors of variables: wff setvar class
Syntax hints:    \/ wo 370    /\ wa 371    = wceq 1444   E.wex 1663    e. wcel 1887    u. cun 3402   U.cuni 4198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-un 3409  df-uni 4199
This theorem is referenced by:  unidif0  4576  unisuc  5499  fvssunirn  5888  fvun  5935  onuninsuci  6667  tc2  8226  fin1a2lem10  8839  fin1a2lem12  8841  incexclem  13894  dprd2da  17675  dmdprdsplit2lem  17678  ordtuni  20206  cmpcld  20417  uncmp  20418  refun0  20530  lfinun  20540  1stckgenlem  20568  filcon  20898  ufildr  20946  alexsubALTlem3  21064  cldsubg  21125  icccmplem2  21841  uniioombllem3  22543  sxbrsigalem0  29093  fiunelcarsg  29148  carsgclctunlem1  29149  carsggect  29150  cvmscld  29996  refssfne  31014  topjoin  31021  mbfresfi  31987  fourierdlem80  38050  isomenndlem  38351
  Copyright terms: Public domain W3C validator