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 4277	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4269	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4160	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4154	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4475	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2761	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4210	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4395	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2761	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2769	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1542  Vcvv 3475   ∖ cdif 3946   ∪ cun 3947   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324

This theorem is referenced by:  undif2  4477  undifr  4483  unidif0  5359  sofld  6187  fresaun  6763  ralxpmap  8890  pwfilem  9177  enp1ilem  9278  difinf  9316  pwfilemOLD  9346  infdif  10204  fin23lem11  10312  fin1a2lem13  10407  axcclem  10452  ttukeylem1  10504  ttukeylem7  10510  fpwwe2lem12  10637  hashbclem  14411  incexclem  15782  ramub1lem1  16959  ramub1lem2  16960  isstruct2  17082  setsdm  17103  mrieqvlemd  17573  mreexmrid  17587  islbs3  20768  lbsextlem4  20774  basdif0  22456  bwth  22914  locfincmp  23030  cldsubg  23615  nulmbl2  25053  volinun  25063  limcdif  25393  ellimc2  25394  limcmpt2  25401  dvreslem  25426  dvaddbr  25455  dvmulbr  25456  lhop  25533  plyeq0  25725  rlimcnp  26470  difeq  31756  ffsrn  31954  symgcom2  32245  esumpad2  33054  measunl  33214  subfacp1lem1  34170  cvmscld  34264  gg-dvmulbr  35175  pibt2  36298  stoweidlem44  44760