Theorem undif1 3903

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3900). 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 3746	. 2
2		invdif 3738	. . 3
3	2	uneq1i 3653	. 2
4		uncom 3647	. . . . 5
5		unvdif 3902	. . . . 5
6	4, 5	eqtri 2486	. . . 4
7	6	ineq2i 3696	. . 3
8		inv1 3812	. . 3
9	7, 8	eqtri 2486	. 2
10	1, 3, 9	3eqtr3i 2494	1

Syntax hints:  =wceq 1395  cvv 3109  \cdif 3472  u.cun 3473  i^icin 3474

This theorem is referenced by:  undif2  3904  unidif0  4625  pwundif  4792  sofld  5460  fresaun  5761  ralxpmap  7488  enp1ilem  7774  difinf  7810  pwfilem  7834  infdif  8610  fin23lem11  8718  fin1a2lem13  8813  axcclem  8858  ttukeylem1  8910  ttukeylem7  8916  fpwwe2lem13  9041  hashbclem  12501  incexclem  13648  ramub1lem1  14544  ramub1lem2  14545  isstruct2  14641  mrieqvlemd  15026  mreexmrid  15040  islbs3  17801  lbsextlem4  17807  basdif0  19454  bwth  19910  locfincmp  20027  cldsubg  20609  nulmbl2  21947  volinun  21956  limcdif  22280  ellimc2  22281  limcmpt2  22288  dvreslem  22313  dvaddbr  22341  dvmulbr  22342  lhop  22417  plyeq0  22608  rlimcnp  23295  difeq  27416  ffsrn  27552  measunl  28187  subfacp1lem1  28623  cvmscld  28718  compne  31349  stoweidlem44  31826

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785