Theorem undif1 4424

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4421). 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 4253	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4245	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4135	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4129	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4423	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2844	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4186	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4348	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2844	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2852	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1537  Vcvv 3494   ∖ cdif 3933   ∪ cun 3934   ∩ cin 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292

This theorem is referenced by:  undif2  4425  unidif0  5260  pwundifOLD  5457  sofld  6044  fresaun  6549  ralxpmap  8460  enp1ilem  8752  difinf  8788  pwfilem  8818  infdif  9631  fin23lem11  9739  fin1a2lem13  9834  axcclem  9879  ttukeylem1  9931  ttukeylem7  9937  fpwwe2lem13  10064  hashbclem  13811  incexclem  15191  ramub1lem1  16362  ramub1lem2  16363  isstruct2  16493  setsdm  16517  mrieqvlemd  16900  mreexmrid  16914  islbs3  19927  lbsextlem4  19933  basdif0  21561  bwth  22018  locfincmp  22134  cldsubg  22719  nulmbl2  24137  volinun  24147  limcdif  24474  ellimc2  24475  limcmpt2  24482  dvreslem  24507  dvaddbr  24535  dvmulbr  24536  lhop  24613  plyeq0  24801  rlimcnp  25543  difeq  30280  ffsrn  30465  symgcom2  30728  esumpad2  31315  measunl  31475  subfacp1lem1  32426  cvmscld  32520  pibt2  34701  stoweidlem44  42349