Theorem undif1 4417

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4413). 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 4228	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4220	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4105	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4099	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4416	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2760	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4158	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4339	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2760	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2768	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1542  Vcvv 3430   ∖ cdif 3887   ∪ cun 3888   ∩ cin 3889

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275

This theorem is referenced by:  undif2  4418  undifr  4424  unidif0  5298  sofld  6146  fresaun  6706  ralxpmap  8838  enp1ilem  9182  difinf  9215  pwfilem  9222  infdif  10124  fin23lem11  10233  fin1a2lem13  10328  axcclem  10373  ttukeylem1  10425  ttukeylem7  10431  fpwwe2lem12  10559  hashbclem  14408  incexclem  15795  ramub1lem1  16991  ramub1lem2  16992  isstruct2  17113  setsdm  17134  mrieqvlemd  17589  mreexmrid  17603  islbs3  21148  lbsextlem4  21154  basdif0  22931  bwth  23388  locfincmp  23504  cldsubg  24089  nulmbl2  25516  volinun  25526  limcdif  25856  ellimc2  25857  limcmpt2  25864  dvreslem  25889  dvaddbr  25918  dvmulbr  25919  lhop  25996  plyeq0  26189  rlimcnp  26945  difeq  32606  ffsrn  32819  symgcom2  33163  esumpad2  34219  measunl  34379  subfacp1lem1  35380  cvmscld  35474  pibt2  37750  stoweidlem44  46493