Theorem undif1 4409

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4405). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)

Assertion

Ref	Expression
undif1	⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Proof of Theorem undif1

Step	Hyp	Ref	Expression
1		undir 4210	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4202	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4093	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4087	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4408	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2766	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4143	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4328	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2766	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2774	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1539  Vcvv 3432   ∖ cdif 3884   ∪ cun 3885   ∩ cin 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257

This theorem is referenced by:  undif2  4410  unidif0  5282  pwundifOLD  5486  sofld  6090  fresaun  6645  ralxpmap  8684  pwfilem  8960  enp1ilem  9051  difinf  9084  pwfilemOLD  9113  infdif  9965  fin23lem11  10073  fin1a2lem13  10168  axcclem  10213  ttukeylem1  10265  ttukeylem7  10271  fpwwe2lem12  10398  hashbclem  14164  incexclem  15548  ramub1lem1  16727  ramub1lem2  16728  isstruct2  16850  setsdm  16871  mrieqvlemd  17338  mreexmrid  17352  islbs3  20417  lbsextlem4  20423  basdif0  22103  bwth  22561  locfincmp  22677  cldsubg  23262  nulmbl2  24700  volinun  24710  limcdif  25040  ellimc2  25041  limcmpt2  25048  dvreslem  25073  dvaddbr  25102  dvmulbr  25103  lhop  25180  plyeq0  25372  rlimcnp  26115  difeq  30865  ffsrn  31064  symgcom2  31353  esumpad2  32024  measunl  32184  subfacp1lem1  33141  cvmscld  33235  pibt2  35588  stoweidlem44  43585