Theorem disjdif 3660

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

Syntax hints:   = wceq 1649   \ cdif 3277   i^i cin 3279   C_ wss 3280   (/)c0 3588

This theorem is referenced by:  undifv  3662  ssdifin0  3669  difdifdir  3675  fresaun  5573  fresaunres2  5574  fvsnun1  5887  fvsnun2  5888  fveqf1o  5988  undifixp  7057  difsnen  7149  undom  7155  sbthlem7  7182  sbthlem8  7183  domunsn  7216  fodomr  7217  domss2  7225  mapdom2  7237  limensuci  7242  phplem2  7246  sucdom2  7262  pssnn  7286  dif1enOLD  7299  dif1en  7300  unfi  7333  marypha1lem  7396  brwdom2  7497  infdifsn  7567  cantnf0  7586  dif1card  7848  ackbij1lem12  8067  ackbij1lem18  8073  ssfin4  8146  canthp1lem1  8483  grothprim  8665  hashgval  11576  hashinf  11578  hashf  11580  hashun2  11612  hashun3  11613  hashssdif  11632  hashfun  11655  hashbclem  11656  hashf1lem2  11660  fsumless  12530  cvgcmpce  12552  incexclem  12571  incexc  12572  setsid  13463  mreexexlem3d  13826  mreexexlem4d  13827  sylow2a  15208  gsumval3a  15467  dprd2da  15555  dpjcntz  15565  dpjdisj  15566  dpjlsm  15567  dpjidcl  15571  ablfac1eu  15586  neitr  17198  nrmsep  17375  regsep2  17394  dfcon2  17435  fbncp  17824  filufint  17905  supnfcls  18005  flimfnfcls  18013  restmetu  18570  xrge0gsumle  18817  volinun  19393  iundisj2  19396  volsup  19403  itg2cnlem2  19607  tdeglem4  19936  amgm  20782  wilthlem2  20805  rpvmasum2  21159  difeq  23951  disjdifprg  23970  iundisj2f  23983  iundisj2fi  24106  esummono  24403  gsumesum  24404  measvuni  24521  measunl  24523  fullfunfnv  25699  fullfunfv  25700  axlowdimlem7  25791  axlowdimlem8  25792  axlowdimlem9  25793  axlowdimlem10  25794  axlowdimlem11  25795  axlowdimlem12  25796  ismblfin  26146  opnbnd  26218  cldbnd  26219  ralxpmap  26632  diophrw  26707  eldioph2lem1  26708  eldioph2lem2  26709  diophren  26764  kelac1  27029  pwssplit1  27056  frlmsslss2  27113  frlmssuvc1  27114  frlmsslsp  27116  enfixsn  27125  islindf4  27176

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-v 2918  df-dif 3283  df-in 3287  df-ss 3294  df-nul 3589