Theorem undif1 4476

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4472). 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 4287	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4279	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4164	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4158	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4475	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2765	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4217	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4398	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2765	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2773	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1540  Vcvv 3480   ∖ cdif 3948   ∪ cun 3949   ∩ cin 3950

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334

This theorem is referenced by:  undif2  4477  undifr  4483  unidif0  5360  sofld  6207  fresaun  6779  ralxpmap  8936  enp1ilem  9312  difinf  9349  pwfilem  9356  infdif  10248  fin23lem11  10357  fin1a2lem13  10452  axcclem  10497  ttukeylem1  10549  ttukeylem7  10555  fpwwe2lem12  10682  hashbclem  14491  incexclem  15872  ramub1lem1  17064  ramub1lem2  17065  isstruct2  17186  setsdm  17207  mrieqvlemd  17672  mreexmrid  17686  islbs3  21157  lbsextlem4  21163  basdif0  22960  bwth  23418  locfincmp  23534  cldsubg  24119  nulmbl2  25571  volinun  25581  limcdif  25911  ellimc2  25912  limcmpt2  25919  dvreslem  25944  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  lhop  26055  plyeq0  26250  rlimcnp  27008  difeq  32537  ffsrn  32740  symgcom2  33104  esumpad2  34057  measunl  34217  subfacp1lem1  35184  cvmscld  35278  pibt2  37418  stoweidlem44  46059