Theorem undif1 4390

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4386). 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 4191	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4183	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4073	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4067	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4389	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2765	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4124	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4309	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2765	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2773	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1543  Vcvv 3408   ∖ cdif 3863   ∪ cun 3864   ∩ cin 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238

This theorem is referenced by:  undif2  4391  unidif0  5251  pwundifOLD  5452  sofld  6050  fresaun  6590  ralxpmap  8577  pwfilem  8855  enp1ilem  8908  difinf  8941  pwfilemOLD  8970  infdif  9823  fin23lem11  9931  fin1a2lem13  10026  axcclem  10071  ttukeylem1  10123  ttukeylem7  10129  fpwwe2lem12  10256  hashbclem  14016  incexclem  15400  ramub1lem1  16579  ramub1lem2  16580  isstruct2  16702  setsdm  16723  mrieqvlemd  17132  mreexmrid  17146  islbs3  20192  lbsextlem4  20198  basdif0  21850  bwth  22307  locfincmp  22423  cldsubg  23008  nulmbl2  24433  volinun  24443  limcdif  24773  ellimc2  24774  limcmpt2  24781  dvreslem  24806  dvaddbr  24835  dvmulbr  24836  lhop  24913  plyeq0  25105  rlimcnp  25848  difeq  30584  ffsrn  30784  symgcom2  31072  esumpad2  31736  measunl  31896  subfacp1lem1  32854  cvmscld  32948  pibt2  35325  stoweidlem44  43260