Theorem disjdif 3886

Description: A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.)

Assertion

Ref	Expression
disjdif	|- ( A i^i ( B \ A ) ) = (/)

Proof of Theorem disjdif

Step	Hyp	Ref	Expression
1		inss1 3703	. 2 |- ( A i^i B ) C_ A
2		inssdif0 3881	. 2 |- ( ( A i^i B ) C_ A <-> ( A i^i ( B \ A ) ) = (/) )
3	1, 2	mpbi 208	1 |- ( A i^i ( B \ A ) ) = (/)

Syntax hints:   = wceq 1383   \ cdif 3458   i^i cin 3460   C_ wss 3461   (/)c0 3770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-v 3097  df-dif 3464  df-in 3468  df-ss 3475  df-nul 3771

This theorem is referenced by:  unvdif  3888  ssdifin0  3895  difdifdir  3901  fresaun  5746  fresaunres2  5747  fvsnun1  6091  fvsnun2  6092  fveqf1o  6190  ralxpmap  7470  undifixp  7507  difsnen  7601  undom  7607  enfixsn  7628  sbthlem7  7635  sbthlem8  7636  domunsn  7669  fodomr  7670  domss2  7678  mapdom2  7690  limensuci  7695  phplem2  7699  sucdom2  7716  pssnn  7740  dif1enOLD  7754  dif1en  7755  unfi  7789  marypha1lem  7895  brwdom2  8002  infdifsn  8076  dif1card  8391  ackbij1lem12  8614  ackbij1lem18  8620  ssfin4  8693  canthp1lem1  9033  grothprim  9215  hashgval  12389  hashinf  12391  hashf  12393  hashun2  12432  hashun3  12433  hashssdif  12456  hashfun  12476  hashbclem  12482  hashf1lem2  12486  fsumless  13591  cvgcmpce  13613  incexclem  13629  incexc  13630  setsid  14654  mreexexlem3d  15024  mreexexlem4d  15025  sylow2a  16617  gsumval3a  16883  gsumval3aOLD  16884  dprd2da  17069  dpjcntz  17079  dpjdisj  17080  dpjlsm  17081  dpjidcl  17085  dpjidclOLD  17092  ablfac1eu  17102  pwssplit1  17683  frlmsslss2  18782  frlmsslss2OLD  18783  frlmssuvc1  18802  frlmssuvc1OLD  18804  frlmsslsp  18806  frlmsslspOLD  18807  islindf4  18850  mdetdiaglem  19077  mdetrlin  19081  mdetrsca  19082  mdetralt  19087  smadiadet  19149  neitr  19658  nrmsep  19835  regsep2  19854  dfcon2  19897  fbncp  20317  filufint  20398  supnfcls  20498  flimfnfcls  20506  restmetu  21067  xrge0gsumle  21315  volinun  21933  iundisj2  21936  volsup  21943  itg2cnlem2  22146  tdeglem4  22435  amgm  23296  wilthlem2  23319  rpvmasum2  23673  axlowdimlem7  24227  axlowdimlem8  24228  axlowdimlem9  24229  axlowdimlem10  24230  axlowdimlem11  24231  axlowdimlem12  24232  difeq  27392  disjdifprg  27412  iundisj2f  27425  resf1o  27529  iundisj2fi  27578  locfinref  27821  esummono  28043  gsumesum  28044  measvuni  28162  measunl  28164  eulerpartlemt  28287  mthmpps  28919  fullfunfnv  29571  fullfunfv  29572  ismblfin  30030  opnbnd  30118  cldbnd  30119  diophrw  30667  eldioph2lem1  30668  eldioph2lem2  30669  diophren  30722  kelac1  30984  sumnnodd  31544