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

Theorem undif1 4187
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4184). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
Assertion
Ref Expression
undif1 ((𝐴𝐵) ∪ 𝐵) = (𝐴𝐵)

Proof of Theorem undif1
StepHypRef Expression
1 undir 4019 . 2 ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2 invdif 4011 . . 3 (𝐴 ∩ (V ∖ 𝐵)) = (𝐴𝐵)
32uneq1i 3906 . 2 ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴𝐵) ∪ 𝐵)
4 uncom 3900 . . . . 5 ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5 unvdif 4186 . . . . 5 (𝐵 ∪ (V ∖ 𝐵)) = V
64, 5eqtri 2782 . . . 4 ((V ∖ 𝐵) ∪ 𝐵) = V
76ineq2i 3954 . . 3 ((𝐴𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴𝐵) ∩ V)
8 inv1 4113 . . 3 ((𝐴𝐵) ∩ V) = (𝐴𝐵)
97, 8eqtri 2782 . 2 ((𝐴𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴𝐵)
101, 3, 93eqtr3i 2790 1 ((𝐴𝐵) ∪ 𝐵) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  Vcvv 3340  cdif 3712  cun 3713  cin 3714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059
This theorem is referenced by:  undif2  4188  unidif0  4987  pwundif  5171  sofld  5739  fresaun  6236  ralxpmap  8073  enp1ilem  8359  difinf  8395  pwfilem  8425  infdif  9223  fin23lem11  9331  fin1a2lem13  9426  axcclem  9471  ttukeylem1  9523  ttukeylem7  9529  fpwwe2lem13  9656  hashbclem  13428  incexclem  14767  ramub1lem1  15932  ramub1lem2  15933  isstruct2  16069  setsdm  16094  mrieqvlemd  16491  mreexmrid  16505  islbs3  19357  lbsextlem4  19363  basdif0  20959  bwth  21415  locfincmp  21531  cldsubg  22115  nulmbl2  23504  volinun  23514  limcdif  23839  ellimc2  23840  limcmpt2  23847  dvreslem  23872  dvaddbr  23900  dvmulbr  23901  lhop  23978  plyeq0  24166  rlimcnp  24891  difeq  29662  ffsrn  29813  esumpad2  30427  measunl  30588  subfacp1lem1  31468  cvmscld  31562  compneOLD  39146  stoweidlem44  40764
  Copyright terms: Public domain W3C validator