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

Theorem undif1 3671
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3668). 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 3558 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  u.  B )  i^i  (
( _V  \  B
)  u.  B ) )
2 invdif 3550 . . 3  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
32uneq1i 3465 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  \  B )  u.  B
)
4 uncom 3459 . . . . 5  |-  ( ( _V  \  B )  u.  B )  =  ( B  u.  ( _V  \  B ) )
5 undifv 3670 . . . . 5  |-  ( B  u.  ( _V  \  B ) )  =  _V
64, 5eqtri 2432 . . . 4  |-  ( ( _V  \  B )  u.  B )  =  _V
76ineq2i 3507 . . 3  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( ( A  u.  B )  i^i  _V )
8 inv1 3622 . . 3  |-  ( ( A  u.  B )  i^i  _V )  =  ( A  u.  B
)
97, 8eqtri 2432 . 2  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( A  u.  B
)
101, 3, 93eqtr3i 2440 1  |-  ( ( A  \  B )  u.  B )  =  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1649   _Vcvv 2924    \ cdif 3285    u. cun 3286    i^i cin 3287
This theorem is referenced by:  undif2  3672  unidif0  4340  pwundif  4458  sofld  5285  fresaun  5581  enp1ilem  7309  difinf  7344  pwfilem  7367  infdif  8053  fin23lem11  8161  fin1a2lem13  8256  axcclem  8301  ttukeylem1  8353  ttukeylem7  8359  fpwwe2lem13  8481  hashbclem  11664  incexclem  12579  ramub1lem1  13357  ramub1lem2  13358  isstruct2  13441  mrieqvlemd  13817  mreexmrid  13831  islbs3  16190  lbsextlem4  16196  basdif0  16981  tgdif0  17020  cldsubg  18101  nulmbl2  19392  volinun  19401  limcdif  19724  ellimc2  19725  limcmpt2  19732  dvreslem  19757  dvaddbr  19785  dvmulbr  19786  lhop  19861  plyeq0  20091  rlimcnp  20765  difeq  23959  measunl  24531  subfacp1lem1  24826  cvmscld  24921  locfincmp  26282  ralxpmap  26640  compne  27518  stoweidlem44  27668
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597
  Copyright terms: Public domain W3C validator