Theorem undif1 4433

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4429). 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 4235	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4227	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4166	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4160	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4432	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2786	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4117	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4351	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2786	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2794	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3454   ∖ cdif 4048   ∩ cin 4092   ∪ cun 4152

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282

This theorem is used by:  undif2  4434  undifr  4442  unidif0  5328  unidif0OLD  5329  sofld  6197  fresaun  6783  ralxpmap  8962  enp1ilem  9307  difinf  9341  pwfilem  9347  infdif  10325  fin23lem11  10434  fin1a2lem13  10529  axcclem  10574  ttukeylem1  10626  ttukeylem7  10632  fpwwe2lem12  10766  hashbclem  14638  incexclem  16049  ramub1lem1  17248  ramub1lem2  17249  isstruct2  17371  setsdm  17392  mrieqvlemd  17853  mreexmrid  17867  islbs3  21484  lbsextlem4  21490  basdif0  23326  bwth  23783  locfincmp  23900  cldsubg  24485  nulmbl2  25912  volinun  25922  limcdif  26251  ellimc2  26252  limcmpt2  26259  dvreslem  26284  dvaddbr  26313  dvmulbr  26314  lhop  26391  plyeq0  26585  rlimcnp  27350  difeq  33213  ffsrn  33416  symgcom2  33744  esumpad2  34799  measunl  34960  subfacp1lem1  36152  cvmscld  36246  pibt2  38608  stoweidlem44  47327