Theorem undif1 4474

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

Syntax hints:   = wceq 1541  Vcvv 3474   ∖ cdif 3944   ∪ cun 3945   ∩ cin 3946

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322

This theorem is referenced by:  undif2  4475  undifr  4481  unidif0  5357  sofld  6183  fresaun  6759  ralxpmap  8886  pwfilem  9173  enp1ilem  9274  difinf  9312  pwfilemOLD  9342  infdif  10200  fin23lem11  10308  fin1a2lem13  10403  axcclem  10448  ttukeylem1  10500  ttukeylem7  10506  fpwwe2lem12  10633  hashbclem  14407  incexclem  15778  ramub1lem1  16955  ramub1lem2  16956  isstruct2  17078  setsdm  17099  mrieqvlemd  17569  mreexmrid  17583  islbs3  20760  lbsextlem4  20766  basdif0  22447  bwth  22905  locfincmp  23021  cldsubg  23606  nulmbl2  25044  volinun  25054  limcdif  25384  ellimc2  25385  limcmpt2  25392  dvreslem  25417  dvaddbr  25446  dvmulbr  25447  lhop  25524  plyeq0  25716  rlimcnp  26459  difeq  31743  ffsrn  31941  symgcom2  32232  esumpad2  33042  measunl  33202  subfacp1lem1  34158  cvmscld  34252  gg-dvmulbr  35163  pibt2  36286  stoweidlem44  44746