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

Theorem undif1 3891
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3888). 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 3744 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  u.  B )  i^i  (
( _V  \  B
)  u.  B ) )
2 invdif 3736 . . 3  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
32uneq1i 3640 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  \  B )  u.  B
)
4 uncom 3634 . . . . 5  |-  ( ( _V  \  B )  u.  B )  =  ( B  u.  ( _V  \  B ) )
5 unvdif 3890 . . . . 5  |-  ( B  u.  ( _V  \  B ) )  =  _V
64, 5eqtri 2483 . . . 4  |-  ( ( _V  \  B )  u.  B )  =  _V
76ineq2i 3683 . . 3  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( ( A  u.  B )  i^i  _V )
8 inv1 3811 . . 3  |-  ( ( A  u.  B )  i^i  _V )  =  ( A  u.  B
)
97, 8eqtri 2483 . 2  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( A  u.  B
)
101, 3, 93eqtr3i 2491 1  |-  ( ( A  \  B )  u.  B )  =  ( A  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398   _Vcvv 3106    \ 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 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784
This theorem is referenced by:  undif2  3892  unidif0  4610  pwundif  4776  sofld  5439  fresaun  5738  ralxpmap  7461  enp1ilem  7746  difinf  7782  pwfilem  7806  infdif  8580  fin23lem11  8688  fin1a2lem13  8783  axcclem  8828  ttukeylem1  8880  ttukeylem7  8886  fpwwe2lem13  9009  hashbclem  12488  incexclem  13733  ramub1lem1  14631  ramub1lem2  14632  isstruct2  14728  mrieqvlemd  15121  mreexmrid  15135  islbs3  17999  lbsextlem4  18005  basdif0  19624  bwth  20080  locfincmp  20196  cldsubg  20778  nulmbl2  22116  volinun  22125  limcdif  22449  ellimc2  22450  limcmpt2  22457  dvreslem  22482  dvaddbr  22510  dvmulbr  22511  lhop  22586  plyeq0  22777  rlimcnp  23496  difeq  27618  ffsrn  27786  esumpad2  28288  measunl  28427  subfacp1lem1  28890  cvmscld  28985  compne  31593  stoweidlem44  32068
  Copyright terms: Public domain W3C validator