Theorem disjdif 3862

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 3681	. 2 |- ( A i^i B ) C_ A
2		inssdif0 3857	. 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 1370   \ cdif 3436   i^i cin 3438   C_ wss 3439   (/)c0 3748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-v 3080  df-dif 3442  df-in 3446  df-ss 3453  df-nul 3749

This theorem is referenced by:  unvdif  3864  ssdifin0  3871  difdifdir  3877  fresaun  5693  fresaunres2  5694  fvsnun1  6025  fvsnun2  6026  fveqf1o  6112  ralxpmap  7375  undifixp  7412  difsnen  7506  undom  7512  enfixsn  7533  sbthlem7  7540  sbthlem8  7541  domunsn  7574  fodomr  7575  domss2  7583  mapdom2  7595  limensuci  7600  phplem2  7604  sucdom2  7621  pssnn  7645  dif1enOLD  7658  dif1en  7659  unfi  7693  marypha1lem  7797  brwdom2  7902  infdifsn  7976  dif1card  8291  ackbij1lem12  8514  ackbij1lem18  8520  ssfin4  8593  canthp1lem1  8933  grothprim  9115  hashgval  12226  hashinf  12228  hashf  12230  hashun2  12267  hashun3  12268  hashssdif  12288  hashfun  12320  hashbclem  12326  hashf1lem2  12330  fsumless  13380  cvgcmpce  13402  incexclem  13420  incexc  13421  setsid  14336  mreexexlem3d  14706  mreexexlem4d  14707  sylow2a  16242  gsumval3a  16503  gsumval3aOLD  16504  dprd2da  16666  dpjcntz  16676  dpjdisj  16677  dpjlsm  16678  dpjidcl  16682  dpjidclOLD  16689  ablfac1eu  16699  pwssplit1  17266  frlmsslss2  18327  frlmsslss2OLD  18328  frlmssuvc1  18347  frlmssuvc1OLD  18349  frlmsslsp  18351  frlmsslspOLD  18352  islindf4  18395  mdetdiaglem  18539  mdetrlin  18543  mdetrsca  18544  mdetralt  18549  smadiadet  18611  neitr  18919  nrmsep  19096  regsep2  19115  dfcon2  19158  fbncp  19547  filufint  19628  supnfcls  19728  flimfnfcls  19736  restmetu  20297  xrge0gsumle  20545  volinun  21163  iundisj2  21166  volsup  21173  itg2cnlem2  21376  tdeglem4  21665  amgm  22520  wilthlem2  22543  rpvmasum2  22897  axlowdimlem7  23366  axlowdimlem8  23367  axlowdimlem9  23368  axlowdimlem10  23369  axlowdimlem11  23370  axlowdimlem12  23371  difeq  26071  disjdifprg  26090  iundisj2f  26103  resf1o  26201  iundisj2fi  26246  esummono  26674  gsumesum  26675  measvuni  26793  measunl  26795  eulerpartlemt  26918  fullfunfnv  28141  fullfunfv  28142  ismblfin  28600  opnbnd  28688  cldbnd  28689  diophrw  29265  eldioph2lem1  29266  eldioph2lem2  29267  diophren  29320  kelac1  29584