Theorem undif1 4442

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4438). 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 4248	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4240	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4126	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4120	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4441	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2792	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4178	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4362	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2792	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2800	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1567  Vcvv 3463   ∖ cdif 3910   ∪ cun 3911   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295

This theorem is referenced by:  undif2  4443  undifr  4449  unidif0  5331  unidif0OLD  5332  sofld  6186  fresaun  6750  ralxpmap  8893  enp1ilem  9237  difinf  9270  pwfilem  9276  infdif  10190  fin23lem11  10300  fin1a2lem13  10395  axcclem  10440  ttukeylem1  10492  ttukeylem7  10498  fpwwe2lem12  10626  hashbclem  14488  incexclem  15889  ramub1lem1  17085  ramub1lem2  17086  isstruct2  17208  setsdm  17229  mrieqvlemd  17684  mreexmrid  17698  islbs3  21256  lbsextlem4  21262  basdif0  23078  bwth  23535  locfincmp  23651  cldsubg  24236  nulmbl2  25663  volinun  25673  limcdif  26003  ellimc2  26004  limcmpt2  26011  dvreslem  26036  dvaddbr  26065  dvmulbr  26066  lhop  26143  plyeq0  26336  rlimcnp  27095  difeq  32804  ffsrn  33013  symgcom2  33344  esumpad2  34390  measunl  34550  subfacp1lem1  35569  cvmscld  35663  pibt2  37950  stoweidlem44  46649