Theorem disjdif 4040

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

Syntax hints:   = wceq 1483   \ cdif 3571   i^i cin 3573   C_ wss 3574   (/)c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916

This theorem is referenced by:  unvdif  4042  ssdifin0  4050  difdifdir  4056  fresaun  6075  fresaunres2  6076  fvsnun1  6448  fvsnun2  6449  fveqf1o  6557  ralxpmap  7907  undifixp  7944  difsnen  8042  undom  8048  enfixsn  8069  sbthlem7  8076  sbthlem8  8077  domunsn  8110  fodomr  8111  domss2  8119  mapdom2  8131  limensuci  8136  phplem2  8140  sucdom2  8156  pssnn  8178  dif1en  8193  unfi  8227  marypha1lem  8339  brwdom2  8478  infdifsn  8554  dif1card  8833  ackbij1lem12  9053  ackbij1lem18  9059  ssfin4  9132  canthp1lem1  9474  grothprim  9656  hashgval  13120  hashinf  13122  hashfxnn0  13124  hashfOLD  13126  hashun2  13172  hashun3  13173  hashssdif  13200  hashfun  13224  hashbclem  13236  hashf1lem2  13240  fsumless  14528  cvgcmpce  14550  incexclem  14568  incexc  14569  fprodsplit1f  14721  setsfun  15893  setsfun0  15894  setsid  15914  mreexexlem3d  16306  mreexexlem4d  16307  sylow2a  18034  gsumval3a  18304  dprd2da  18441  dpjcntz  18451  dpjdisj  18452  dpjlsm  18453  dpjidcl  18457  ablfac1eu  18472  pwssplit1  19059  frlmsslss2  20114  frlmssuvc1  20133  frlmsslsp  20135  islindf4  20177  mdetdiaglem  20404  mdetrlin  20408  mdetrsca  20409  mdetralt  20414  smadiadet  20476  neitr  20984  nrmsep  21161  regsep2  21180  dfconn2  21222  fbncp  21643  filufint  21724  supnfcls  21824  flimfnfcls  21832  restmetu  22375  xrge0gsumle  22636  volinun  23314  iundisj2  23317  volsup  23324  itg2cnlem2  23529  tdeglem4  23820  amgm  24717  wilthlem2  24795  rpvmasum2  25201  axlowdimlem7  25828  axlowdimlem8  25829  axlowdimlem9  25830  axlowdimlem10  25831  axlowdimlem11  25832  axlowdimlem12  25833  difeq  29355  disjdifprg  29388  iundisj2f  29403  padct  29497  resf1o  29505  iundisj2fi  29556  fprodeq02  29569  locfinref  29908  esummono  30116  esumpad  30117  gsumesum  30121  ldgenpisyslem1  30226  measvuni  30277  measunl  30279  pmeasmono  30386  eulerpartlemt  30433  tgoldbachgtde  30738  mthmpps  31479  noextendseq  31820  noetalem2  31864  noetalem3  31865  fullfunfnv  32053  fullfunfv  32054  opnbnd  32320  cldbnd  32321  poimirlem6  33415  poimirlem7  33416  poimirlem15  33424  poimirlem16  33425  poimirlem19  33428  poimirlem22  33431  poimirlem27  33436  ismblfin  33450  diophrw  37322  eldioph2lem1  37323  eldioph2lem2  37324  diophren  37377  kelac1  37633  sumnnodd  39862  sge0ss  40629  meassle  40680  meaunle  40681  meadif  40696  meaiininclem  40700  isomenndlem  40744