Theorem undif1 4437

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4433). 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 4240	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4232	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4118	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4112	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4436	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2786	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4170	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4355	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2786	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2794	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1570  Vcvv 3455   ∖ cdif 3902   ∪ cun 3903   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287

This theorem is referenced by:  undif2  4438  undifr  4444  unidif0  5330  unidif0OLD  5331  sofld  6185  fresaun  6749  ralxpmap  8890  enp1ilem  9234  difinf  9267  pwfilem  9273  infdif  10187  fin23lem11  10296  fin1a2lem13  10391  axcclem  10436  ttukeylem1  10488  ttukeylem7  10494  fpwwe2lem12  10622  hashbclem  14485  incexclem  15886  ramub1lem1  17081  ramub1lem2  17082  isstruct2  17204  setsdm  17225  mrieqvlemd  17680  mreexmrid  17694  islbs3  21279  lbsextlem4  21285  basdif0  23110  bwth  23567  locfincmp  23683  cldsubg  24268  nulmbl2  25695  volinun  25705  limcdif  26035  ellimc2  26036  limcmpt2  26043  dvreslem  26068  dvaddbr  26097  dvmulbr  26098  lhop  26175  plyeq0  26368  rlimcnp  27130  difeq  32864  ffsrn  33073  symgcom2  33404  esumpad2  34446  measunl  34606  subfacp1lem1  35671  cvmscld  35765  pibt2  38063  stoweidlem44  46758