Theorem disjdif 4236

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	⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅

Proof of Theorem disjdif

Step	Hyp	Ref	Expression
1		inss1 4029	. 2 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
2		inssdif0 4148	. 2 ⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 ↔ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅)
3	1, 2	mpbi 221	1 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅

Syntax hints:   = wceq 1637   ∖ cdif 3766   ∩ cin 3768   ⊆ wss 3769  ∅c0 4116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-dif 3772  df-in 3776  df-ss 3783  df-nul 4117

This theorem is referenced by:  unvdif  4238  ssdifin0  4246  difdifdir  4252  fresaun  6290  fresaunres2  6291  fvsnun1  6673  fvsnun2  6674  fveqf1o  6781  ralxpmap  8144  undifixp  8181  difsnen  8281  undom  8287  enfixsn  8308  sbthlem7  8315  sbthlem8  8316  domunsn  8349  fodomr  8350  domss2  8358  mapdom2  8370  limensuci  8375  phplem2  8379  sucdom2  8395  pssnn  8417  dif1en  8432  unfi  8466  marypha1lem  8578  brwdom2  8717  infdifsn  8801  dif1card  9116  ackbij1lem12  9338  ackbij1lem18  9344  ssfin4  9417  canthp1lem1  9759  grothprim  9941  hashgval  13340  hashinf  13342  hashfxnn0  13344  hashfOLD  13346  hashun2  13390  hashun3  13391  hashssdif  13417  hashfun  13441  hashbclem  13453  hashf1lem2  13457  fsumless  14750  cvgcmpce  14772  incexclem  14790  incexc  14791  fprodsplit1f  14941  setsfun  16104  setsfun0  16105  setsid  16125  mreexexlem3d  16511  mreexexlem4d  16512  sylow2a  18235  gsumval3a  18505  dprd2da  18643  dpjcntz  18653  dpjdisj  18654  dpjlsm  18655  dpjidcl  18659  ablfac1eu  18674  pwssplit1  19266  frlmsslss2  20324  frlmssuvc1  20343  frlmsslsp  20345  islindf4  20387  mdetdiaglem  20615  mdetrlin  20619  mdetrsca  20620  mdetralt  20625  smadiadet  20688  neitr  21198  nrmsep  21375  regsep2  21394  dfconn2  21436  fbncp  21856  filufint  21937  supnfcls  22037  flimfnfcls  22045  restmetu  22588  xrge0gsumle  22849  volinun  23527  iundisj2  23530  volsup  23537  itg2cnlem2  23743  tdeglem4  24034  amgm  24931  wilthlem2  25009  rpvmasum2  25415  axlowdimlem7  26042  axlowdimlem8  26043  axlowdimlem9  26044  axlowdimlem10  26045  axlowdimlem11  26046  axlowdimlem12  26047  difeq  29680  disjdifprg  29713  iundisj2f  29728  padct  29824  resf1o  29832  iundisj2fi  29883  fprodeq02  29896  locfinref  30233  esummono  30441  esumpad  30442  gsumesum  30446  ldgenpisyslem1  30551  measvuni  30602  measunl  30604  pmeasmono  30711  eulerpartlemt  30758  tgoldbachgtde  31063  mthmpps  31802  noextendseq  32141  noetalem2  32185  noetalem3  32186  fullfunfnv  32374  fullfunfv  32375  opnbnd  32641  cldbnd  32642  poimirlem6  33728  poimirlem7  33729  poimirlem15  33737  poimirlem16  33738  poimirlem19  33741  poimirlem22  33744  poimirlem27  33749  ismblfin  33763  diophrw  37824  eldioph2lem1  37825  eldioph2lem2  37826  diophren  37879  kelac1  38134  sumnnodd  40342  sge0ss  41108  meassle  41159  meaunle  41160  meadif  41175  meaiininclem  41182  isomenndlem  41226