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

Theorem undif1 3889
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3886). 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 3732 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  u.  B )  i^i  (
( _V  \  B
)  u.  B ) )
2 invdif 3724 . . 3  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
32uneq1i 3639 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  \  B )  u.  B
)
4 uncom 3633 . . . . 5  |-  ( ( _V  \  B )  u.  B )  =  ( B  u.  ( _V  \  B ) )
5 unvdif 3888 . . . . 5  |-  ( B  u.  ( _V  \  B ) )  =  _V
64, 5eqtri 2472 . . . 4  |-  ( ( _V  \  B )  u.  B )  =  _V
76ineq2i 3682 . . 3  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( ( A  u.  B )  i^i  _V )
8 inv1 3798 . . 3  |-  ( ( A  u.  B )  i^i  _V )  =  ( A  u.  B
)
97, 8eqtri 2472 . 2  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( A  u.  B
)
101, 3, 93eqtr3i 2480 1  |-  ( ( A  \  B )  u.  B )  =  ( A  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383   _Vcvv 3095    \ cdif 3458    u. cun 3459    i^i cin 3460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771
This theorem is referenced by:  undif2  3890  unidif0  4610  pwundif  4777  sofld  5445  fresaun  5746  ralxpmap  7470  enp1ilem  7756  difinf  7792  pwfilem  7816  infdif  8592  fin23lem11  8700  fin1a2lem13  8795  axcclem  8840  ttukeylem1  8892  ttukeylem7  8898  fpwwe2lem13  9023  hashbclem  12483  incexclem  13630  ramub1lem1  14526  ramub1lem2  14527  isstruct2  14623  mrieqvlemd  15008  mreexmrid  15022  islbs3  17780  lbsextlem4  17786  basdif0  19432  bwth  19888  locfincmp  20005  cldsubg  20587  nulmbl2  21925  volinun  21934  limcdif  22258  ellimc2  22259  limcmpt2  22266  dvreslem  22291  dvaddbr  22319  dvmulbr  22320  lhop  22395  plyeq0  22586  rlimcnp  23273  difeq  27394  ffsrn  27530  measunl  28165  subfacp1lem1  28601  cvmscld  28696  compne  31303  stoweidlem44  31780
  Copyright terms: Public domain W3C validator