Theorem undif1 4416

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4412). 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 4227	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4219	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4104	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4098	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4415	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2759	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4157	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4338	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2759	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2767	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1542  Vcvv 3429   ∖ cdif 3886   ∪ cun 3887   ∩ cin 3888

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274

This theorem is referenced by:  undif2  4417  undifr  4423  unidif0  5301  unidif0OLD  5302  sofld  6151  fresaun  6711  ralxpmap  8844  enp1ilem  9188  difinf  9221  pwfilem  9228  infdif  10130  fin23lem11  10239  fin1a2lem13  10334  axcclem  10379  ttukeylem1  10431  ttukeylem7  10437  fpwwe2lem12  10565  hashbclem  14414  incexclem  15801  ramub1lem1  16997  ramub1lem2  16998  isstruct2  17119  setsdm  17140  mrieqvlemd  17595  mreexmrid  17609  islbs3  21153  lbsextlem4  21159  basdif0  22918  bwth  23375  locfincmp  23491  cldsubg  24076  nulmbl2  25503  volinun  25513  limcdif  25843  ellimc2  25844  limcmpt2  25851  dvreslem  25876  dvaddbr  25905  dvmulbr  25906  lhop  25983  plyeq0  26176  rlimcnp  26929  difeq  32588  ffsrn  32801  symgcom2  33145  esumpad2  34200  measunl  34360  subfacp1lem1  35361  cvmscld  35455  pibt2  37733  stoweidlem44  46472