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

Theorem undif1 3759
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3756). 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 3604 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  u.  B )  i^i  (
( _V  \  B
)  u.  B ) )
2 invdif 3596 . . 3  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
32uneq1i 3511 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  \  B )  u.  B
)
4 uncom 3505 . . . . 5  |-  ( ( _V  \  B )  u.  B )  =  ( B  u.  ( _V  \  B ) )
5 unvdif 3758 . . . . 5  |-  ( B  u.  ( _V  \  B ) )  =  _V
64, 5eqtri 2463 . . . 4  |-  ( ( _V  \  B )  u.  B )  =  _V
76ineq2i 3554 . . 3  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( ( A  u.  B )  i^i  _V )
8 inv1 3669 . . 3  |-  ( ( A  u.  B )  i^i  _V )  =  ( A  u.  B
)
97, 8eqtri 2463 . 2  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( A  u.  B
)
101, 3, 93eqtr3i 2471 1  |-  ( ( A  \  B )  u.  B )  =  ( A  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   _Vcvv 2977    \ cdif 3330    u. cun 3331    i^i cin 3332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643
This theorem is referenced by:  undif2  3760  unidif0  4470  pwundif  4633  sofld  5291  fresaun  5587  ralxpmap  7267  enp1ilem  7551  difinf  7587  pwfilem  7610  infdif  8383  fin23lem11  8491  fin1a2lem13  8586  axcclem  8631  ttukeylem1  8683  ttukeylem7  8689  fpwwe2lem13  8814  hashbclem  12210  incexclem  13304  ramub1lem1  14092  ramub1lem2  14093  isstruct2  14188  mrieqvlemd  14572  mreexmrid  14586  islbs3  17241  lbsextlem4  17247  basdif0  18563  tgdif0  18602  bwth  19018  cldsubg  19686  nulmbl2  21023  volinun  21032  limcdif  21356  ellimc2  21357  limcmpt2  21364  dvreslem  21389  dvaddbr  21417  dvmulbr  21418  lhop  21493  plyeq0  21684  rlimcnp  22364  difeq  25904  ffsrn  26034  measunl  26635  subfacp1lem1  27072  cvmscld  27167  locfincmp  28581  compne  29701  stoweidlem44  29844
  Copyright terms: Public domain W3C validator