Theorem undif1 4338

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4335). 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 4173	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4165	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4056	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4050	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4337	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2819	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4106	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4268	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2819	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2827	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1522  Vcvv 3437   ∖ cdif 3856   ∪ cun 3857   ∩ cin 3858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212

This theorem is referenced by:  undif2  4339  unidif0  5151  pwundif  5345  sofld  5920  fresaun  6417  ralxpmap  8309  enp1ilem  8598  difinf  8634  pwfilem  8664  infdif  9477  fin23lem11  9585  fin1a2lem13  9680  axcclem  9725  ttukeylem1  9777  ttukeylem7  9783  fpwwe2lem13  9910  hashbclem  13658  incexclem  15024  ramub1lem1  16191  ramub1lem2  16192  isstruct2  16322  setsdm  16346  mrieqvlemd  16729  mreexmrid  16743  islbs3  19617  lbsextlem4  19623  basdif0  21245  bwth  21702  locfincmp  21818  cldsubg  22402  nulmbl2  23820  volinun  23830  limcdif  24157  ellimc2  24158  limcmpt2  24165  dvreslem  24190  dvaddbr  24218  dvmulbr  24219  lhop  24296  plyeq0  24484  rlimcnp  25225  difeq  29969  ffsrn  30153  symgcom2  30387  esumpad2  30932  measunl  31092  subfacp1lem1  32035  cvmscld  32129  pibt2  34248  stoweidlem44  41891