Theorem undif1 4430

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4426). 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 4233	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4225	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4111	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4105	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4429	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2784	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4163	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4348	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2784	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2792	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3451   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280

This theorem is used by:  undif2  4431  undifr  4439  unidif0  5321  unidif0OLD  5322  sofld  6179  fresaun  6751  ralxpmap  8917  enp1ilem  9262  difinf  9296  pwfilem  9302  infdif  10279  fin23lem11  10388  fin1a2lem13  10483  axcclem  10528  ttukeylem1  10580  ttukeylem7  10586  fpwwe2lem12  10720  hashbclem  14590  incexclem  15998  ramub1lem1  17197  ramub1lem2  17198  isstruct2  17320  setsdm  17341  mrieqvlemd  17796  mreexmrid  17810  islbs3  21426  lbsextlem4  21432  basdif0  23264  bwth  23721  locfincmp  23838  cldsubg  24423  nulmbl2  25850  volinun  25860  limcdif  26189  ellimc2  26190  limcmpt2  26197  dvreslem  26222  dvaddbr  26251  dvmulbr  26252  lhop  26329  plyeq0  26523  rlimcnp  27286  difeq  33107  ffsrn  33313  symgcom2  33638  esumpad2  34681  measunl  34842  subfacp1lem1  35923  cvmscld  36017  pibt2  38320  stoweidlem44  47023