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

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

Proof of Theorem undif1
StepHypRef Expression
1 undir 3834 . 2 ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2 invdif 3826 . . 3 (𝐴 ∩ (V ∖ 𝐵)) = (𝐴𝐵)
32uneq1i 3724 . 2 ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴𝐵) ∪ 𝐵)
4 uncom 3718 . . . . 5 ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5 unvdif 3993 . . . . 5 (𝐵 ∪ (V ∖ 𝐵)) = V
64, 5eqtri 2631 . . . 4 ((V ∖ 𝐵) ∪ 𝐵) = V
76ineq2i 3772 . . 3 ((𝐴𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴𝐵) ∩ V)
8 inv1 3921 . . 3 ((𝐴𝐵) ∩ V) = (𝐴𝐵)
97, 8eqtri 2631 . 2 ((𝐴𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴𝐵)
101, 3, 93eqtr3i 2639 1 ((𝐴𝐵) ∪ 𝐵) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  Vcvv 3172  cdif 3536  cun 3537  cin 3538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874
This theorem is referenced by:  undif2  3995  unidif0  4759  pwundif  4935  sofld  5486  fresaun  5973  ralxpmap  7770  enp1ilem  8056  difinf  8092  pwfilem  8120  infdif  8891  fin23lem11  8999  fin1a2lem13  9094  axcclem  9139  ttukeylem1  9191  ttukeylem7  9197  fpwwe2lem13  9320  hashbclem  13045  incexclem  14353  ramub1lem1  15514  ramub1lem2  15515  isstruct2  15650  setsdm  15670  mrieqvlemd  16058  mreexmrid  16072  islbs3  18922  lbsextlem4  18928  basdif0  20510  bwth  20965  locfincmp  21081  cldsubg  21666  nulmbl2  23028  volinun  23038  limcdif  23363  ellimc2  23364  limcmpt2  23371  dvreslem  23396  dvaddbr  23424  dvmulbr  23425  lhop  23500  plyeq0  23688  rlimcnp  24409  difeq  28545  ffsrn  28698  esumpad2  29251  measunl  29412  subfacp1lem1  30221  cvmscld  30315  compne  37461  stoweidlem44  38734
  Copyright terms: Public domain W3C validator