Theorem undif1 4430

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4426). 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 4241	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4233	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4118	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4112	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4429	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2760	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4171	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4352	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2760	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2768	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1542  Vcvv 3442   ∖ cdif 3900   ∪ cun 3901   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288

This theorem is referenced by:  undif2  4431  undifr  4437  unidif0  5307  sofld  6153  fresaun  6713  ralxpmap  8846  enp1ilem  9190  difinf  9223  pwfilem  9230  infdif  10130  fin23lem11  10239  fin1a2lem13  10334  axcclem  10379  ttukeylem1  10431  ttukeylem7  10437  fpwwe2lem12  10565  hashbclem  14387  incexclem  15771  ramub1lem1  16966  ramub1lem2  16967  isstruct2  17088  setsdm  17109  mrieqvlemd  17564  mreexmrid  17578  islbs3  21122  lbsextlem4  21128  basdif0  22909  bwth  23366  locfincmp  23482  cldsubg  24067  nulmbl2  25505  volinun  25515  limcdif  25845  ellimc2  25846  limcmpt2  25853  dvreslem  25878  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  lhop  25989  plyeq0  26184  rlimcnp  26943  difeq  32605  ffsrn  32818  symgcom2  33178  esumpad2  34234  measunl  34394  subfacp1lem1  35395  cvmscld  35489  pibt2  37672  stoweidlem44  46402