Theorem undif1 4404

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4400). 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 4215	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4207	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4094	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4088	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4403	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2762	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4146	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4326	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2762	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2770	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1547  Vcvv 3431   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262

This theorem is referenced by:  undif2  4405  undifr  4411  unidif0  5288  unidif0OLD  5289  sofld  6138  fresaun  6698  ralxpmap  8834  enp1ilem  9178  difinf  9211  pwfilem  9218  infdif  10121  fin23lem11  10230  fin1a2lem13  10325  axcclem  10370  ttukeylem1  10422  ttukeylem7  10428  fpwwe2lem12  10556  hashbclem  14405  incexclem  15792  ramub1lem1  16988  ramub1lem2  16989  isstruct2  17110  setsdm  17131  mrieqvlemd  17586  mreexmrid  17600  islbs3  21148  lbsextlem4  21154  basdif0  22936  bwth  23393  locfincmp  23509  cldsubg  24094  nulmbl2  25521  volinun  25531  limcdif  25861  ellimc2  25862  limcmpt2  25869  dvreslem  25894  dvaddbr  25923  dvmulbr  25924  lhop  26001  plyeq0  26194  rlimcnp  26947  difeq  32606  ffsrn  32820  symgcom2  33165  esumpad2  34240  measunl  34400  subfacp1lem1  35407  cvmscld  35501  pibt2  37779  stoweidlem44  46487