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 2788	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4170	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4355	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2788	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2796	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3457   ∖ cdif 3903   ∪ cun 3904   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287

This theorem is used by:  undif2  4438  undifr  4446  unidif0  5332  unidif0OLD  5333  sofld  6187  fresaun  6753  ralxpmap  8900  enp1ilem  9245  difinf  9278  pwfilem  9284  infdif  10207  fin23lem11  10316  fin1a2lem13  10411  axcclem  10456  ttukeylem1  10508  ttukeylem7  10514  fpwwe2lem12  10642  hashbclem  14507  incexclem  15913  ramub1lem1  17108  ramub1lem2  17109  isstruct2  17231  setsdm  17252  mrieqvlemd  17707  mreexmrid  17721  islbs3  21329  lbsextlem4  21335  basdif0  23160  bwth  23617  locfincmp  23734  cldsubg  24319  nulmbl2  25746  volinun  25756  limcdif  26086  ellimc2  26087  limcmpt2  26094  dvreslem  26119  dvaddbr  26148  dvmulbr  26149  lhop  26226  plyeq0  26419  rlimcnp  27181  difeq  32935  ffsrn  33143  symgcom2  33468  esumpad2  34510  measunl  34671  subfacp1lem1  35708  cvmscld  35802  pibt2  38120  stoweidlem44  46816