Theorem undif1 4429

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4425). 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 4231	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4223	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4162	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4156	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4428	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2783	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4113	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4347	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2783	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2791	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

This proof depends on syntax axioms:   = wceq 1569  Vcvv 3450   ∖ cdif 4044   ∩ cin 4088   ∪ cun 4148

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278

This theorem is used by:  undif2  4430  undifr  4438  unidif0  5321  unidif0OLD  5322  sofld  6181  fresaun  6758  ralxpmap  8931  enp1ilem  9276  difinf  9310  pwfilem  9316  infdif  10293  fin23lem11  10402  fin1a2lem13  10497  axcclem  10542  ttukeylem1  10594  ttukeylem7  10600  fpwwe2lem12  10734  hashbclem  14604  incexclem  16014  ramub1lem1  17213  ramub1lem2  17214  isstruct2  17336  setsdm  17357  mrieqvlemd  17812  mreexmrid  17826  islbs3  21442  lbsextlem4  21448  basdif0  23280  bwth  23737  locfincmp  23854  cldsubg  24439  nulmbl2  25866  volinun  25876  limcdif  26205  ellimc2  26206  limcmpt2  26213  dvreslem  26238  dvaddbr  26267  dvmulbr  26268  lhop  26345  plyeq0  26539  rlimcnp  27302  difeq  33165  ffsrn  33370  symgcom2  33695  esumpad2  34738  measunl  34899  subfacp1lem1  36034  cvmscld  36128  pibt2  38449  stoweidlem44  47162