Theorem disjdif 3899

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 3718	. 2 |- ( A i^i B ) C_ A
2		inssdif0 3894	. 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 1379   \ cdif 3473   i^i cin 3475   C_ wss 3476   (/)c0 3785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490  df-nul 3786

This theorem is referenced by:  unvdif  3901  ssdifin0  3908  difdifdir  3914  fresaun  5755  fresaunres2  5756  fvsnun1  6095  fvsnun2  6096  fveqf1o  6192  ralxpmap  7468  undifixp  7505  difsnen  7599  undom  7605  enfixsn  7626  sbthlem7  7633  sbthlem8  7634  domunsn  7667  fodomr  7668  domss2  7676  mapdom2  7688  limensuci  7693  phplem2  7697  sucdom2  7714  pssnn  7738  dif1enOLD  7751  dif1en  7752  unfi  7786  marypha1lem  7892  brwdom2  7998  infdifsn  8072  dif1card  8387  ackbij1lem12  8610  ackbij1lem18  8616  ssfin4  8689  canthp1lem1  9029  grothprim  9211  hashgval  12375  hashinf  12377  hashf  12379  hashun2  12418  hashun3  12419  hashssdif  12439  hashfun  12460  hashbclem  12466  hashf1lem2  12470  fsumless  13572  cvgcmpce  13594  incexclem  13610  incexc  13611  setsid  14530  mreexexlem3d  14900  mreexexlem4d  14901  sylow2a  16442  gsumval3a  16705  gsumval3aOLD  16706  dprd2da  16890  dpjcntz  16900  dpjdisj  16901  dpjlsm  16902  dpjidcl  16906  dpjidclOLD  16913  ablfac1eu  16923  pwssplit1  17500  frlmsslss2  18588  frlmsslss2OLD  18589  frlmssuvc1  18608  frlmssuvc1OLD  18610  frlmsslsp  18612  frlmsslspOLD  18613  islindf4  18656  mdetdiaglem  18883  mdetrlin  18887  mdetrsca  18888  mdetralt  18893  smadiadet  18955  neitr  19463  nrmsep  19640  regsep2  19659  dfcon2  19702  fbncp  20091  filufint  20172  supnfcls  20272  flimfnfcls  20280  restmetu  20841  xrge0gsumle  21089  volinun  21707  iundisj2  21710  volsup  21717  itg2cnlem2  21920  tdeglem4  22209  amgm  23064  wilthlem2  23087  rpvmasum2  23441  axlowdimlem7  23943  axlowdimlem8  23944  axlowdimlem9  23945  axlowdimlem10  23946  axlowdimlem11  23947  axlowdimlem12  23948  difeq  27106  disjdifprg  27125  iundisj2f  27138  resf1o  27241  iundisj2fi  27286  esummono  27722  gsumesum  27723  measvuni  27841  measunl  27843  eulerpartlemt  27966  fullfunfnv  29189  fullfunfv  29190  ismblfin  29648  opnbnd  29736  cldbnd  29737  diophrw  30312  eldioph2lem1  30313  eldioph2lem2  30314  diophren  30367  kelac1  30629  sumnnodd  31188