Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  undif1 Unicode version

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
StepHypRef Expression
1 undir 3746 . 2
2 invdif 3738 . . 3
32uneq1i 3653 . 2
4 uncom 3647 . . . . 5
5 unvdif 3902 . . . . 5
64, 5eqtri 2486 . . . 4
76ineq2i 3696 . . 3
8 inv1 3812 . . 3
97, 8eqtri 2486 . 2
101, 3, 93eqtr3i 2494 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator