Theorem undif1 4430

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4426). 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 4233	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4225	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4111	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4105	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4429	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2783	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4163	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4348	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2783	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2791	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3450   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280

This theorem is used by:  undif2  4431  undifr  4439  unidif0  5324  unidif0OLD  5325  sofld  6180  fresaun  6746  ralxpmap  8903  enp1ilem  9248  difinf  9281  pwfilem  9287  infdif  10210  fin23lem11  10319  fin1a2lem13  10414  axcclem  10459  ttukeylem1  10511  ttukeylem7  10517  fpwwe2lem12  10651  hashbclem  14517  incexclem  15925  ramub1lem1  17118  ramub1lem2  17119  isstruct2  17241  setsdm  17262  mrieqvlemd  17717  mreexmrid  17731  islbs3  21342  lbsextlem4  21348  basdif0  23178  bwth  23635  locfincmp  23752  cldsubg  24337  nulmbl2  25764  volinun  25774  limcdif  26103  ellimc2  26104  limcmpt2  26111  dvreslem  26136  dvaddbr  26165  dvmulbr  26166  lhop  26243  plyeq0  26437  rlimcnp  27202  difeq  32993  ffsrn  33199  symgcom2  33524  esumpad2  34566  measunl  34727  subfacp1lem1  35758  cvmscld  35852  pibt2  38171  stoweidlem44  46872