Theorem disjdif 3816

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 3632	. 2 |- ( A i^i B ) C_ A
2		inssdif0 3811	. 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 1399   \ cdif 3386   i^i cin 3388   C_ wss 3389   (/)c0 3711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-v 3036  df-dif 3392  df-in 3396  df-ss 3403  df-nul 3712

This theorem is referenced by:  unvdif  3818  ssdifin0  3825  difdifdir  3831  fresaun  5664  fresaunres2  5665  fvsnun1  6008  fvsnun2  6009  fveqf1o  6106  ralxpmap  7387  undifixp  7424  difsnen  7518  undom  7524  enfixsn  7545  sbthlem7  7552  sbthlem8  7553  domunsn  7586  fodomr  7587  domss2  7595  mapdom2  7607  limensuci  7612  phplem2  7616  sucdom2  7632  pssnn  7654  dif1en  7668  unfi  7702  marypha1lem  7808  brwdom2  7914  infdifsn  7987  dif1card  8301  ackbij1lem12  8524  ackbij1lem18  8530  ssfin4  8603  canthp1lem1  8941  grothprim  9123  hashgval  12310  hashinf  12312  hashf  12314  hashun2  12354  hashun3  12355  hashssdif  12379  hashfun  12399  hashbclem  12405  hashf1lem2  12409  fsumless  13612  cvgcmpce  13634  incexclem  13650  incexc  13651  setsid  14677  mreexexlem3d  15053  mreexexlem4d  15054  sylow2a  16756  gsumval3a  17022  gsumval3aOLD  17023  dprd2da  17204  dpjcntz  17214  dpjdisj  17215  dpjlsm  17216  dpjidcl  17220  dpjidclOLD  17227  ablfac1eu  17237  pwssplit1  17818  frlmsslss2  18894  frlmsslss2OLD  18895  frlmssuvc1  18914  frlmsslsp  18916  islindf4  18958  mdetdiaglem  19185  mdetrlin  19189  mdetrsca  19190  mdetralt  19195  smadiadet  19257  neitr  19767  nrmsep  19944  regsep2  19963  dfcon2  20005  fbncp  20425  filufint  20506  supnfcls  20606  flimfnfcls  20614  restmetu  21175  xrge0gsumle  21423  volinun  22041  iundisj2  22044  volsup  22051  itg2cnlem2  22254  tdeglem4  22543  amgm  23437  wilthlem2  23460  rpvmasum2  23814  axlowdimlem7  24372  axlowdimlem8  24373  axlowdimlem9  24374  axlowdimlem10  24375  axlowdimlem11  24376  axlowdimlem12  24377  difeq  27534  disjdifprg  27565  iundisj2f  27579  padct  27695  resf1o  27703  iundisj2fi  27755  locfinref  27998  esummono  28202  esumpad  28203  gsumesum  28207  measvuni  28341  measunl  28343  eulerpartlemt  28493  mthmpps  29131  fullfunfnv  29749  fullfunfv  29750  ismblfin  30220  opnbnd  30309  cldbnd  30310  diophrw  30857  eldioph2lem1  30858  eldioph2lem2  30859  diophren  30912  kelac1  31175  fprodsplit1f  31759  sumnnodd  31802