Theorem disjdif 3746

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 3565	. 2 |- ( A i^i B ) C_ A
2		inssdif0 3741	. 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 1369   \ cdif 3320   i^i cin 3322   C_ wss 3323   (/)c0 3632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2969  df-dif 3326  df-in 3330  df-ss 3337  df-nul 3633

This theorem is referenced by:  unvdif  3748  ssdifin0  3755  difdifdir  3761  fresaun  5577  fresaunres2  5578  fvsnun1  5908  fvsnun2  5909  fveqf1o  5995  ralxpmap  7254  undifixp  7291  difsnen  7385  undom  7391  enfixsn  7412  sbthlem7  7419  sbthlem8  7420  domunsn  7453  fodomr  7454  domss2  7462  mapdom2  7474  limensuci  7479  phplem2  7483  sucdom2  7499  pssnn  7523  dif1enOLD  7536  dif1en  7537  unfi  7571  marypha1lem  7675  brwdom2  7780  infdifsn  7854  dif1card  8169  ackbij1lem12  8392  ackbij1lem18  8398  ssfin4  8471  canthp1lem1  8811  grothprim  8993  hashgval  12098  hashinf  12100  hashf  12102  hashun2  12138  hashun3  12139  hashssdif  12159  hashfun  12191  hashbclem  12197  hashf1lem2  12201  fsumless  13251  cvgcmpce  13273  incexclem  13291  incexc  13292  setsid  14207  mreexexlem3d  14576  mreexexlem4d  14577  sylow2a  16109  gsumval3a  16370  gsumval3aOLD  16371  dprd2da  16529  dpjcntz  16539  dpjdisj  16540  dpjlsm  16541  dpjidcl  16545  dpjidclOLD  16552  ablfac1eu  16562  pwssplit1  17117  frlmsslss2  18174  frlmsslss2OLD  18175  frlmssuvc1  18194  frlmssuvc1OLD  18196  frlmsslsp  18198  frlmsslspOLD  18199  islindf4  18242  mdet1  18383  mdetrlin  18384  mdetrsca  18385  mdetralt  18389  smadiadet  18451  neitr  18759  nrmsep  18936  regsep2  18955  dfcon2  18998  fbncp  19387  filufint  19468  supnfcls  19568  flimfnfcls  19576  restmetu  20137  xrge0gsumle  20385  volinun  21002  iundisj2  21005  volsup  21012  itg2cnlem2  21215  tdeglem4  21504  amgm  22359  wilthlem2  22382  rpvmasum2  22736  axlowdimlem7  23145  axlowdimlem8  23146  axlowdimlem9  23147  axlowdimlem10  23148  axlowdimlem11  23149  axlowdimlem12  23150  difeq  25850  disjdifprg  25870  iundisj2f  25883  resf1o  25981  iundisj2fi  26032  esummono  26461  gsumesum  26462  measvuni  26580  measunl  26582  eulerpartlemt  26706  fullfunfnv  27928  fullfunfv  27929  ismblfin  28385  opnbnd  28473  cldbnd  28474  diophrw  29050  eldioph2lem1  29051  eldioph2lem2  29052  diophren  29105  kelac1  29369  mdetdiaglem  30824