Theorem undif1 4435

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4431). 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 4246	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4238	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4123	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4117	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4434	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2752	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4176	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4357	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2752	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2760	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1540  Vcvv 3444   ∖ cdif 3908   ∪ cun 3909   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293

This theorem is referenced by:  undif2  4436  undifr  4442  unidif0  5310  sofld  6148  fresaun  6713  ralxpmap  8846  enp1ilem  9199  difinf  9236  pwfilem  9243  infdif  10137  fin23lem11  10246  fin1a2lem13  10341  axcclem  10386  ttukeylem1  10438  ttukeylem7  10444  fpwwe2lem12  10571  hashbclem  14393  incexclem  15778  ramub1lem1  16973  ramub1lem2  16974  isstruct2  17095  setsdm  17116  mrieqvlemd  17566  mreexmrid  17580  islbs3  21041  lbsextlem4  21047  basdif0  22816  bwth  23273  locfincmp  23389  cldsubg  23974  nulmbl2  25413  volinun  25423  limcdif  25753  ellimc2  25754  limcmpt2  25761  dvreslem  25786  dvaddbr  25816  dvmulbr  25817  dvmulbrOLD  25818  lhop  25897  plyeq0  26092  rlimcnp  26851  difeq  32420  ffsrn  32625  symgcom2  33014  esumpad2  34019  measunl  34179  subfacp1lem1  35139  cvmscld  35233  pibt2  37378  stoweidlem44  46015