Theorem disjdif 3812

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

Syntax hints:   = wceq 1437   \ cdif 3376   i^i cin 3378   C_ wss 3379   (/)c0 3704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-v 3024  df-dif 3382  df-in 3386  df-ss 3393  df-nul 3705

This theorem is referenced by:  unvdif  3814  ssdifin0  3822  difdifdir  3828  fresaun  5714  fresaunres2  5715  fvsnun1  6058  fvsnun2  6059  fveqf1o  6159  ralxpmap  7476  undifixp  7513  difsnen  7607  undom  7613  enfixsn  7634  sbthlem7  7641  sbthlem8  7642  domunsn  7675  fodomr  7676  domss2  7684  mapdom2  7696  limensuci  7701  phplem2  7705  sucdom2  7721  pssnn  7743  dif1en  7757  unfi  7791  marypha1lem  7900  brwdom2  8041  infdifsn  8114  dif1card  8393  ackbij1lem12  8612  ackbij1lem18  8618  ssfin4  8691  canthp1lem1  9028  grothprim  9210  hashgval  12468  hashinf  12470  hashf  12472  hashun2  12512  hashun3  12513  hashssdif  12537  hashfun  12557  hashbclem  12563  hashf1lem2  12567  fsumless  13799  cvgcmpce  13821  incexclem  13837  incexc  13838  fprodsplit1f  13987  setsid  15107  mreexexlem3d  15495  mreexexlem4d  15496  sylow2a  17214  gsumval3a  17480  dprd2da  17618  dpjcntz  17628  dpjdisj  17629  dpjlsm  17630  dpjidcl  17634  ablfac1eu  17649  pwssplit1  18225  frlmsslss2  19275  frlmssuvc1  19294  frlmsslsp  19296  islindf4  19338  mdetdiaglem  19565  mdetrlin  19569  mdetrsca  19570  mdetralt  19575  smadiadet  19637  neitr  20138  nrmsep  20315  regsep2  20334  dfcon2  20376  fbncp  20796  filufint  20877  supnfcls  20977  flimfnfcls  20985  restmetu  21527  xrge0gsumle  21793  volinun  22441  iundisj2  22444  volsup  22451  itg2cnlem2  22662  tdeglem4  22951  amgm  23858  wilthlem2  23936  rpvmasum2  24292  axlowdimlem7  24920  axlowdimlem8  24921  axlowdimlem9  24922  axlowdimlem10  24923  axlowdimlem11  24924  axlowdimlem12  24925  difeq  28094  disjdifprg  28131  iundisj2f  28146  padct  28257  resf1o  28265  iundisj2fi  28323  locfinref  28620  esummono  28827  esumpad  28828  gsumesum  28832  ldgenpisyslem1  28937  measvuni  28988  measunl  28990  pmeasmono  29109  eulerpartlemt  29156  mthmpps  30172  fullfunfnv  30662  fullfunfv  30663  opnbnd  30930  cldbnd  30931  poimirlem6  31853  poimirlem7  31854  poimirlem15  31862  poimirlem16  31863  poimirlem19  31866  poimirlem22  31869  poimirlem25  31872  poimirlem27  31874  ismblfin  31888  diophrw  35513  eldioph2lem1  35514  eldioph2lem2  35515  diophren  35568  kelac1  35834  sumnnodd  37593  sge0ss  38105  meassle  38152  meaunle  38153  isomenndlem  38202