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

Theorem undif1 3639
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3636). 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 3526 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  u.  B )  i^i  (
( _V  \  B
)  u.  B ) )
2 invdif 3518 . . 3  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
32uneq1i 3433 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  \  B )  u.  B
)
4 uncom 3427 . . . . 5  |-  ( ( _V  \  B )  u.  B )  =  ( B  u.  ( _V  \  B ) )
5 undifv 3638 . . . . 5  |-  ( B  u.  ( _V  \  B ) )  =  _V
64, 5eqtri 2400 . . . 4  |-  ( ( _V  \  B )  u.  B )  =  _V
76ineq2i 3475 . . 3  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( ( A  u.  B )  i^i  _V )
8 inv1 3590 . . 3  |-  ( ( A  u.  B )  i^i  _V )  =  ( A  u.  B
)
97, 8eqtri 2400 . 2  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( A  u.  B
)
101, 3, 93eqtr3i 2408 1  |-  ( ( A  \  B )  u.  B )  =  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1649   _Vcvv 2892    \ cdif 3253    u. cun 3254    i^i cin 3255
This theorem is referenced by:  undif2  3640  unidif0  4306  pwundif  4424  sofld  5251  fresaun  5547  enp1ilem  7271  difinf  7306  pwfilem  7329  infdif  8015  fin23lem11  8123  fin1a2lem13  8218  axcclem  8263  ttukeylem1  8315  ttukeylem7  8321  fpwwe2lem13  8443  hashbclem  11621  incexclem  12536  ramub1lem1  13314  ramub1lem2  13315  isstruct2  13398  mrieqvlemd  13774  mreexmrid  13788  islbs3  16147  lbsextlem4  16153  basdif0  16934  tgdif0  16973  cldsubg  18054  nulmbl2  19291  volinun  19300  limcdif  19623  ellimc2  19624  limcmpt2  19631  dvreslem  19656  dvaddbr  19684  dvmulbr  19685  lhop  19760  plyeq0  19990  rlimcnp  20664  difeq  23835  measunl  24357  subfacp1lem1  24637  cvmscld  24732  locfincmp  26068  ralxpmap  26426  compne  27304  stoweidlem44  27454
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
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 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-ral 2647  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565
  Copyright terms: Public domain W3C validator