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

Theorem undif1 3529
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3526). 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 3418 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  u.  B )  i^i  (
( _V  \  B
)  u.  B ) )
2 invdif 3410 . . 3  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
32uneq1i 3325 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  \  B )  u.  B
)
4 uncom 3319 . . . . 5  |-  ( ( _V  \  B )  u.  B )  =  ( B  u.  ( _V  \  B ) )
5 undifv 3528 . . . . 5  |-  ( B  u.  ( _V  \  B ) )  =  _V
64, 5eqtri 2303 . . . 4  |-  ( ( _V  \  B )  u.  B )  =  _V
76ineq2i 3367 . . 3  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( ( A  u.  B )  i^i  _V )
8 inv1 3481 . . 3  |-  ( ( A  u.  B )  i^i  _V )  =  ( A  u.  B
)
97, 8eqtri 2303 . 2  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( A  u.  B
)
101, 3, 93eqtr3i 2311 1  |-  ( ( A  \  B )  u.  B )  =  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1623   _Vcvv 2788    \ cdif 3149    u. cun 3150    i^i cin 3151
This theorem is referenced by:  undif2  3530  unidif0  4183  pwundif  4300  sofld  5121  fresaun  5412  enp1ilem  7092  difinf  7127  pwfilem  7150  infdif  7835  fin23lem11  7943  fin1a2lem13  8038  axcclem  8083  ttukeylem1  8136  ttukeylem7  8142  fpwwe2lem13  8264  hashbclem  11390  incexclem  12295  ramub1lem1  13073  ramub1lem2  13074  isstruct2  13157  mrieqvlemd  13531  mreexmrid  13545  islbs3  15908  lbsextlem4  15914  basdif0  16691  tgdif0  16730  cldsubg  17793  nulmbl2  18894  volinun  18903  limcdif  19226  ellimc2  19227  limcmpt2  19234  dvreslem  19259  dvaddbr  19287  dvmulbr  19288  lhop  19363  plyeq0  19593  rlimcnp  20260  difeq  23128  pwundif2  23186  subfacp1lem1  23710  cvmscld  23804  locfincmp  26304  ralxpmap  26761  compne  27642  stoweidlem44  27793
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456
  Copyright terms: Public domain W3C validator