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

Theorem undif1 3870
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3867). 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 3722 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  u.  B )  i^i  (
( _V  \  B
)  u.  B ) )
2 invdif 3714 . . 3  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
32uneq1i 3616 . 2  |-  ( ( A  i^i  ( _V 
\  B ) )  u.  B )  =  ( ( A  \  B )  u.  B
)
4 uncom 3610 . . . . 5  |-  ( ( _V  \  B )  u.  B )  =  ( B  u.  ( _V  \  B ) )
5 unvdif 3869 . . . . 5  |-  ( B  u.  ( _V  \  B ) )  =  _V
64, 5eqtri 2451 . . . 4  |-  ( ( _V  \  B )  u.  B )  =  _V
76ineq2i 3661 . . 3  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( ( A  u.  B )  i^i  _V )
8 inv1 3789 . . 3  |-  ( ( A  u.  B )  i^i  _V )  =  ( A  u.  B
)
97, 8eqtri 2451 . 2  |-  ( ( A  u.  B )  i^i  ( ( _V 
\  B )  u.  B ) )  =  ( A  u.  B
)
101, 3, 93eqtr3i 2459 1  |-  ( ( A  \  B )  u.  B )  =  ( A  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   _Vcvv 3081    \ cdif 3433    u. cun 3434    i^i cin 3435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762
This theorem is referenced by:  undif2  3871  unidif0  4594  pwundif  4757  sofld  5300  fresaun  5768  ralxpmap  7526  enp1ilem  7808  difinf  7844  pwfilem  7871  infdif  8640  fin23lem11  8748  fin1a2lem13  8843  axcclem  8888  ttukeylem1  8940  ttukeylem7  8946  fpwwe2lem13  9068  hashbclem  12613  incexclem  13882  ramub1lem1  14972  ramub1lem2  14973  isstruct2  15118  mrieqvlemd  15523  mreexmrid  15537  islbs3  18366  lbsextlem4  18372  basdif0  19955  bwth  20412  locfincmp  20528  cldsubg  21112  nulmbl2  22477  volinun  22486  limcdif  22818  ellimc2  22819  limcmpt2  22826  dvreslem  22851  dvaddbr  22879  dvmulbr  22880  lhop  22955  plyeq0  23152  rlimcnp  23878  difeq  28138  ffsrn  28308  esumpad2  28873  measunl  29034  subfacp1lem1  29898  cvmscld  29992  compne  36651  stoweidlem44  37725
  Copyright terms: Public domain W3C validator