Theorem disjdif 3850

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 3663	. 2 |- ( A i^i B ) C_ A
2		inssdif0 3845	. 2 |- ( ( A i^i B ) C_ A <-> ( A i^i ( B \ A ) ) = (/) )
3	1, 2	mpbi 213	1 |- ( A i^i ( B \ A ) ) = (/)

Syntax hints:   = wceq 1454   \ cdif 3412   i^i cin 3414   C_ wss 3415   (/)c0 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-v 3058  df-dif 3418  df-in 3422  df-ss 3429  df-nul 3743

This theorem is referenced by:  unvdif  3852  ssdifin0  3860  difdifdir  3866  fresaun  5776  fresaunres2  5777  fvsnun1  6122  fvsnun2  6123  fveqf1o  6224  ralxpmap  7546  undifixp  7583  difsnen  7679  undom  7685  enfixsn  7706  sbthlem7  7713  sbthlem8  7714  domunsn  7747  fodomr  7748  domss2  7756  mapdom2  7768  limensuci  7773  phplem2  7777  sucdom2  7793  pssnn  7815  dif1en  7829  unfi  7863  marypha1lem  7972  brwdom2  8113  infdifsn  8187  dif1card  8466  ackbij1lem12  8686  ackbij1lem18  8692  ssfin4  8765  canthp1lem1  9102  grothprim  9284  hashgval  12549  hashinf  12551  hashf  12553  hashun2  12593  hashun3  12594  hashssdif  12620  hashfun  12641  hashbclem  12647  hashf1lem2  12651  fsumless  13904  cvgcmpce  13926  incexclem  13942  incexc  13943  fprodsplit1f  14092  setsid  15212  mreexexlem3d  15600  mreexexlem4d  15601  sylow2a  17319  gsumval3a  17585  dprd2da  17723  dpjcntz  17733  dpjdisj  17734  dpjlsm  17735  dpjidcl  17739  ablfac1eu  17754  pwssplit1  18330  frlmsslss2  19381  frlmssuvc1  19400  frlmsslsp  19402  islindf4  19444  mdetdiaglem  19671  mdetrlin  19675  mdetrsca  19676  mdetralt  19681  smadiadet  19743  neitr  20244  nrmsep  20421  regsep2  20440  dfcon2  20482  fbncp  20902  filufint  20983  supnfcls  21083  flimfnfcls  21091  restmetu  21633  xrge0gsumle  21899  volinun  22547  iundisj2  22550  volsup  22557  itg2cnlem2  22768  tdeglem4  23057  amgm  23964  wilthlem2  24042  rpvmasum2  24398  axlowdimlem7  25026  axlowdimlem8  25027  axlowdimlem9  25028  axlowdimlem10  25029  axlowdimlem11  25030  axlowdimlem12  25031  difeq  28199  disjdifprg  28233  iundisj2f  28248  padct  28355  resf1o  28363  iundisj2fi  28421  locfinref  28716  esummono  28923  esumpad  28924  gsumesum  28928  ldgenpisyslem1  29033  measvuni  29084  measunl  29086  pmeasmono  29205  eulerpartlemt  29252  mthmpps  30268  fullfunfnv  30761  fullfunfv  30762  opnbnd  31029  cldbnd  31030  poimirlem6  31990  poimirlem7  31991  poimirlem15  31999  poimirlem16  32000  poimirlem19  32003  poimirlem22  32006  poimirlem25  32009  poimirlem27  32011  ismblfin  32025  diophrw  35645  eldioph2lem1  35646  eldioph2lem2  35647  diophren  35700  kelac1  35965  sumnnodd  37747  sge0ss  38291  meassle  38338  meaunle  38339  isomenndlem  38388