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

Theorem undif1 3531
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3528). 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 3420 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  u.  B )  i^i  (
( _V  \  B
)  u.  B ) )
2 invdif 3412 . . 3  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
32uneq1i 3327 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  \  B )  u.  B
)
4 uncom 3321 . . . . 5  |-  ( ( _V  \  B )  u.  B )  =  ( B  u.  ( _V  \  B ) )
5 undifv 3530 . . . . 5  |-  ( B  u.  ( _V  \  B ) )  =  _V
64, 5eqtri 2305 . . . 4  |-  ( ( _V  \  B )  u.  B )  =  _V
76ineq2i 3369 . . 3  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( ( A  u.  B )  i^i  _V )
8 inv1 3483 . . 3  |-  ( ( A  u.  B )  i^i  _V )  =  ( A  u.  B
)
97, 8eqtri 2305 . 2  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( A  u.  B
)
101, 3, 93eqtr3i 2313 1  |-  ( ( A  \  B )  u.  B )  =  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1624   _Vcvv 2790    \ cdif 3151    u. cun 3152    i^i cin 3153
This theorem is referenced by:  undif2  3532  unidif0  4183  pwundif  4300  sofld  5121  fresaun  5378  enp1ilem  7088  difinf  7123  pwfilem  7146  infdif  7831  fin23lem11  7939  fin1a2lem13  8034  axcclem  8079  ttukeylem1  8132  ttukeylem7  8138  fpwwe2lem13  8260  hashbclem  11385  incexclem  12290  ramub1lem1  13068  ramub1lem2  13069  isstruct2  13152  mrieqvlemd  13526  mreexmrid  13540  islbs3  15903  lbsextlem4  15909  basdif0  16686  tgdif0  16725  cldsubg  17788  nulmbl2  18889  volinun  18898  limcdif  19221  ellimc2  19222  limcmpt2  19229  dvreslem  19254  dvaddbr  19282  dvmulbr  19283  lhop  19358  plyeq0  19588  rlimcnp  20255  subfacp1lem1  23115  cvmscld  23209  locfincmp  25704  ralxpmap  26161  compne  27042  stoweidlem44  27193
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458
  Copyright terms: Public domain W3C validator