Theorem undif1 4043

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4040). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)

Assertion

Ref	Expression
undif1	|- ( ( A \ B ) u. B ) = ( A u. B )

Proof of Theorem undif1

Step	Hyp	Ref	Expression
1		undir 3876	. 2 |- ( ( A i^i ( _V \ B ) ) u. B ) = ( ( A u. B ) i^i ( ( _V \ B ) u. B ) )
2		invdif 3868	. . 3 |- ( A i^i ( _V \ B ) ) = ( A \ B )
3	2	uneq1i 3763	. 2 |- ( ( A i^i ( _V \ B ) ) u. B ) = ( ( A \ B ) u. B )
4		uncom 3757	. . . . 5 |- ( ( _V \ B ) u. B ) = ( B u. ( _V \ B ) )
5		unvdif 4042	. . . . 5 |- ( B u. ( _V \ B ) ) = _V
6	4, 5	eqtri 2644	. . . 4 |- ( ( _V \ B ) u. B ) = _V
7	6	ineq2i 3811	. . 3 |- ( ( A u. B ) i^i ( ( _V \ B ) u. B ) ) = ( ( A u. B ) i^i _V )
8		inv1 3970	. . 3 |- ( ( A u. B ) i^i _V ) = ( A u. B )
9	7, 8	eqtri 2644	. 2 |- ( ( A u. B ) i^i ( ( _V \ B ) u. B ) ) = ( A u. B )
10	1, 3, 9	3eqtr3i 2652	1 |- ( ( A \ B ) u. B ) = ( A u. B )

Syntax hints:   = wceq 1483   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916

This theorem is referenced by:  undif2  4044  unidif0  4838  pwundif  5021  sofld  5581  fresaun  6075  ralxpmap  7907  enp1ilem  8194  difinf  8230  pwfilem  8260  infdif  9031  fin23lem11  9139  fin1a2lem13  9234  axcclem  9279  ttukeylem1  9331  ttukeylem7  9337  fpwwe2lem13  9464  hashbclem  13236  incexclem  14568  ramub1lem1  15730  ramub1lem2  15731  isstruct2  15867  setsdm  15892  mrieqvlemd  16289  mreexmrid  16303  islbs3  19155  lbsextlem4  19161  basdif0  20757  bwth  21213  locfincmp  21329  cldsubg  21914  nulmbl2  23304  volinun  23314  limcdif  23640  ellimc2  23641  limcmpt2  23648  dvreslem  23673  dvaddbr  23701  dvmulbr  23702  lhop  23779  plyeq0  23967  rlimcnp  24692  difeq  29355  ffsrn  29504  esumpad2  30118  measunl  30279  subfacp1lem1  31161  cvmscld  31255  compneOLD  38644  stoweidlem44  40261