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

Theorem undif1 3542
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3539). 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 3431 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  u.  B )  i^i  (
( _V  \  B
)  u.  B ) )
2 invdif 3423 . . 3  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
32uneq1i 3338 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  \  B )  u.  B
)
4 uncom 3332 . . . . 5  |-  ( ( _V  \  B )  u.  B )  =  ( B  u.  ( _V  \  B ) )
5 undifv 3541 . . . . 5  |-  ( B  u.  ( _V  \  B ) )  =  _V
64, 5eqtri 2316 . . . 4  |-  ( ( _V  \  B )  u.  B )  =  _V
76ineq2i 3380 . . 3  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( ( A  u.  B )  i^i  _V )
8 inv1 3494 . . 3  |-  ( ( A  u.  B )  i^i  _V )  =  ( A  u.  B
)
97, 8eqtri 2316 . 2  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( A  u.  B
)
101, 3, 93eqtr3i 2324 1  |-  ( ( A  \  B )  u.  B )  =  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1632   _Vcvv 2801    \ cdif 3162    u. cun 3163    i^i cin 3164
This theorem is referenced by:  undif2  3543  unidif0  4199  pwundif  4316  sofld  5137  fresaun  5428  enp1ilem  7108  difinf  7143  pwfilem  7166  infdif  7851  fin23lem11  7959  fin1a2lem13  8054  axcclem  8099  ttukeylem1  8152  ttukeylem7  8158  fpwwe2lem13  8280  hashbclem  11406  incexclem  12311  ramub1lem1  13089  ramub1lem2  13090  isstruct2  13173  mrieqvlemd  13547  mreexmrid  13561  islbs3  15924  lbsextlem4  15930  basdif0  16707  tgdif0  16746  cldsubg  17809  nulmbl2  18910  volinun  18919  limcdif  19242  ellimc2  19243  limcmpt2  19250  dvreslem  19275  dvaddbr  19303  dvmulbr  19304  lhop  19379  plyeq0  19609  rlimcnp  20276  difeq  23144  pwundif2  23202  subfacp1lem1  23725  cvmscld  23819  locfincmp  26407  ralxpmap  26864  compne  27745  stoweidlem44  27896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469
  Copyright terms: Public domain W3C validator