Theorem disjdif 3739

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 3558	. 2 |- ( A i^i B ) C_ A
2		inssdif0 3734	. 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 1362   \ cdif 3313   i^i cin 3315   C_ wss 3316   (/)c0 3625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-v 2964  df-dif 3319  df-in 3323  df-ss 3330  df-nul 3626

This theorem is referenced by:  unvdif  3741  ssdifin0  3748  difdifdir  3754  fresaun  5570  fresaunres2  5571  fvsnun1  5900  fvsnun2  5901  fveqf1o  5987  ralxpmap  7250  undifixp  7287  difsnen  7381  undom  7387  enfixsn  7408  sbthlem7  7415  sbthlem8  7416  domunsn  7449  fodomr  7450  domss2  7458  mapdom2  7470  limensuci  7475  phplem2  7479  sucdom2  7495  pssnn  7519  dif1enOLD  7532  dif1en  7533  unfi  7567  marypha1lem  7671  brwdom2  7776  infdifsn  7850  dif1card  8165  ackbij1lem12  8388  ackbij1lem18  8394  ssfin4  8467  canthp1lem1  8807  grothprim  8989  hashgval  12090  hashinf  12092  hashf  12094  hashun2  12130  hashun3  12131  hashssdif  12151  hashfun  12183  hashbclem  12189  hashf1lem2  12193  fsumless  13242  cvgcmpce  13264  incexclem  13282  incexc  13283  setsid  14198  mreexexlem3d  14567  mreexexlem4d  14568  sylow2a  16098  gsumval3a  16359  gsumval3aOLD  16360  dprd2da  16515  dpjcntz  16525  dpjdisj  16526  dpjlsm  16527  dpjidcl  16531  dpjidclOLD  16538  ablfac1eu  16548  pwssplit1  17062  frlmsslss2  18041  frlmsslss2OLD  18042  frlmssuvc1  18061  frlmssuvc1OLD  18063  frlmsslsp  18065  frlmsslspOLD  18066  islindf4  18109  mdet1  18250  mdetrlin  18251  mdetrsca  18252  mdetralt  18256  smadiadet  18318  neitr  18626  nrmsep  18803  regsep2  18822  dfcon2  18865  fbncp  19254  filufint  19335  supnfcls  19435  flimfnfcls  19443  restmetu  20004  xrge0gsumle  20252  volinun  20869  iundisj2  20872  volsup  20879  itg2cnlem2  21082  tdeglem4  21414  amgm  22269  wilthlem2  22292  rpvmasum2  22646  axlowdimlem7  23017  axlowdimlem8  23018  axlowdimlem9  23019  axlowdimlem10  23020  axlowdimlem11  23021  axlowdimlem12  23022  difeq  25723  disjdifprg  25743  iundisj2f  25756  resf1o  25855  iundisj2fi  25904  esummono  26363  gsumesum  26364  measvuni  26482  measunl  26484  eulerpartlemt  26602  fullfunfnv  27824  fullfunfv  27825  ismblfin  28276  opnbnd  28364  cldbnd  28365  diophrw  28942  eldioph2lem1  28943  eldioph2lem2  28944  diophren  28997  kelac1  29261  mdetdiaglem  30665