Theorem undif1 4428

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4424). 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 4239	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4231	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4116	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4110	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4427	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2759	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4169	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4350	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2759	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2767	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1541  Vcvv 3440   ∖ cdif 3898   ∪ cun 3899   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286

This theorem is referenced by:  undif2  4429  undifr  4435  unidif0  5305  sofld  6145  fresaun  6705  ralxpmap  8834  enp1ilem  9178  difinf  9211  pwfilem  9218  infdif  10118  fin23lem11  10227  fin1a2lem13  10322  axcclem  10367  ttukeylem1  10419  ttukeylem7  10425  fpwwe2lem12  10553  hashbclem  14375  incexclem  15759  ramub1lem1  16954  ramub1lem2  16955  isstruct2  17076  setsdm  17097  mrieqvlemd  17552  mreexmrid  17566  islbs3  21110  lbsextlem4  21116  basdif0  22897  bwth  23354  locfincmp  23470  cldsubg  24055  nulmbl2  25493  volinun  25503  limcdif  25833  ellimc2  25834  limcmpt2  25841  dvreslem  25866  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  lhop  25977  plyeq0  26172  rlimcnp  26931  difeq  32593  ffsrn  32807  symgcom2  33166  esumpad2  34213  measunl  34373  subfacp1lem1  35373  cvmscld  35467  pibt2  37622  stoweidlem44  46288