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

Theorem undif1 3902
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3899). 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 3747 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  u.  B )  i^i  (
( _V  \  B
)  u.  B ) )
2 invdif 3739 . . 3  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
32uneq1i 3654 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  \  B )  u.  B
)
4 uncom 3648 . . . . 5  |-  ( ( _V  \  B )  u.  B )  =  ( B  u.  ( _V  \  B ) )
5 unvdif 3901 . . . . 5  |-  ( B  u.  ( _V  \  B ) )  =  _V
64, 5eqtri 2496 . . . 4  |-  ( ( _V  \  B )  u.  B )  =  _V
76ineq2i 3697 . . 3  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( ( A  u.  B )  i^i  _V )
8 inv1 3812 . . 3  |-  ( ( A  u.  B )  i^i  _V )  =  ( A  u.  B
)
97, 8eqtri 2496 . 2  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( A  u.  B
)
101, 3, 93eqtr3i 2504 1  |-  ( ( A  \  B )  u.  B )  =  ( A  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379   _Vcvv 3113    \ cdif 3473    u. cun 3474    i^i cin 3475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786
This theorem is referenced by:  undif2  3903  unidif0  4620  pwundif  4787  sofld  5455  fresaun  5756  ralxpmap  7468  enp1ilem  7754  difinf  7790  pwfilem  7814  infdif  8589  fin23lem11  8697  fin1a2lem13  8792  axcclem  8837  ttukeylem1  8889  ttukeylem7  8895  fpwwe2lem13  9020  hashbclem  12467  incexclem  13611  ramub1lem1  14403  ramub1lem2  14404  isstruct2  14499  mrieqvlemd  14884  mreexmrid  14898  islbs3  17601  lbsextlem4  17607  basdif0  19249  tgdif0  19288  bwth  19704  cldsubg  20372  nulmbl2  21710  volinun  21719  limcdif  22043  ellimc2  22044  limcmpt2  22051  dvreslem  22076  dvaddbr  22104  dvmulbr  22105  lhop  22180  plyeq0  22371  rlimcnp  23051  difeq  27118  ffsrn  27252  measunl  27855  subfacp1lem1  28291  cvmscld  28386  locfincmp  29804  compne  30955  stoweidlem44  31372
  Copyright terms: Public domain W3C validator