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

Theorem undif1 3490
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3487). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
Assertion
Ref Expression
undif1  |-  ( ( A  \  B )  u.  B )  =  ( A  u.  B
)

Proof of Theorem undif1
StepHypRef Expression
1 undir 3379 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  u.  B )  i^i  (
( _V  \  B
)  u.  B ) )
2 invdif 3371 . . 3  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
32uneq1i 3286 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  \  B )  u.  B
)
4 uncom 3280 . . . . 5  |-  ( ( _V  \  B )  u.  B )  =  ( B  u.  ( _V  \  B ) )
5 undifv 3489 . . . . 5  |-  ( B  u.  ( _V  \  B ) )  =  _V
64, 5eqtri 2276 . . . 4  |-  ( ( _V  \  B )  u.  B )  =  _V
76ineq2i 3328 . . 3  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( ( A  u.  B )  i^i  _V )
8 inv1 3442 . . 3  |-  ( ( A  u.  B )  i^i  _V )  =  ( A  u.  B
)
97, 8eqtri 2276 . 2  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( A  u.  B
)
101, 3, 93eqtr3i 2284 1  |-  ( ( A  \  B )  u.  B )  =  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1619   _Vcvv 2757    \ cdif 3110    u. cun 3111    i^i cin 3112
This theorem is referenced by:  undif2  3491  unidif0  4141  pwundif  4258  sofld  5095  fresaun  5336  enp1ilem  7046  difinf  7081  pwfilem  7104  infdif  7789  fin23lem11  7897  fin1a2lem13  7992  axcclem  8037  ttukeylem1  8090  ttukeylem7  8096  fpwwe2lem13  8218  hashbclem  11341  ramub1lem1  13021  ramub1lem2  13022  isstruct2  13105  mrieqvlemd  13479  mreexmrid  13493  islbs3  15856  lbsextlem4  15862  basdif0  16639  tgdif0  16678  cldsubg  17741  nulmbl2  18842  volinun  18851  limcdif  19174  ellimc2  19175  limcmpt2  19182  dvreslem  19207  dvaddbr  19235  dvmulbr  19236  lhop  19311  plyeq0  19541  rlimcnp  20208  subfacp1lem1  23068  cvmscld  23162  locfincmp  25657  ralxpmap  26114  compne  26996  stoweidlem44  27114
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417
  Copyright terms: Public domain W3C validator