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

Theorem undif1 3435
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3432). 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 3325 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  u.  B )  i^i  (
( _V  \  B
)  u.  B ) )
2 invdif 3317 . . 3  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
32uneq1i 3235 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  \  B )  u.  B
)
4 uncom 3229 . . . . 5  |-  ( ( _V  \  B )  u.  B )  =  ( B  u.  ( _V  \  B ) )
5 undifv 3434 . . . . 5  |-  ( B  u.  ( _V  \  B ) )  =  _V
64, 5eqtri 2273 . . . 4  |-  ( ( _V  \  B )  u.  B )  =  _V
76ineq2i 3275 . . 3  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( ( A  u.  B )  i^i  _V )
8 inv1 3388 . . 3  |-  ( ( A  u.  B )  i^i  _V )  =  ( A  u.  B
)
97, 8eqtri 2273 . 2  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( A  u.  B
)
101, 3, 93eqtr3i 2281 1  |-  ( ( A  \  B )  u.  B )  =  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1619   _Vcvv 2727    \ cdif 3075    u. cun 3076    i^i cin 3077
This theorem is referenced by:  undif2  3436  unidif0  4077  pwundif  4193  sofld  5028  fresaun  5269  enp1ilem  6977  difinf  7012  pwfilem  7034  infdif  7719  fin23lem11  7827  fin1a2lem13  7922  axcclem  7967  ttukeylem1  8020  ttukeylem7  8026  fpwwe2lem13  8144  hashbclem  11267  ramub1lem1  12947  ramub1lem2  12948  isstruct2  13031  islbs3  15742  lbsextlem4  15746  basdif0  16523  tgdif0  16562  cldsubg  17625  nulmbl2  18726  volinun  18735  limcdif  19058  ellimc2  19059  limcmpt2  19066  dvreslem  19091  dvaddbr  19119  dvmulbr  19120  lhop  19195  plyeq0  19425  rlimcnp  20092  subfacp1lem1  22881  cvmscld  22975  locfincmp  25470  ralxpmap  25927  compne  26809  stoweidlem44  26927
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363
  Copyright terms: Public domain W3C validator