Theorem disjdif 4473

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 4227	. 2 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
2		inssdif0 4371	. 2 ⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 ↔ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅)
3	1, 2	mpbi 229	1 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅

Syntax hints:   = wceq 1533   ∖ cdif 3941   ∩ cin 3943   ⊆ wss 3944  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-dif 3947  df-in 3951  df-ss 3961  df-nul 4323

This theorem is referenced by:  disjdifr  4474  unvdif  4476  difdifdir  4493  fresaun  6768  fresaunres2  6769  fvsnun2  7192  undifixp  8953  undom  9084  undomOLD  9085  enfixsn  9106  sucdom2OLD  9107  sbthlem7  9114  sbthlem8  9115  fodomr  9153  domss2  9161  mapdom2  9173  sucdom2  9231  phplem2OLD  9243  pssnnOLD  9290  dif1ennnALT  9302  unfiOLD  9338  marypha1lem  9458  brwdom2  9598  infdifsn  9682  ackbij1lem12  10256  ssfin4  10335  hashinf  14330  hashfxnn0  14332  hashun2  14378  hashun3  14379  hashssdif  14407  hashfun  14432  hashf1lem2  14453  fsumless  15778  cvgcmpce  15800  incexclem  15818  incexc  15819  fprodsplit1f  15970  mreexexlem3d  17629  sylow2a  19586  gsumval3a  19870  dprd2da  20011  dpjcntz  20021  dpjdisj  20022  dpjlsm  20023  dpjidcl  20027  ablfac1eu  20042  pwssplit1  20956  frlmsslss2  21726  frlmssuvc1  21745  psdmul  22113  mdetdiaglem  22544  mdetrlin  22548  mdetrsca  22549  mdetralt  22554  smadiadet  22616  nrmsep  23305  dfconn2  23367  fbncp  23787  filufint  23868  supnfcls  23968  flimfnfcls  23976  xrge0gsumle  24793  iundisj2  25522  volsup  25529  itg2cnlem2  25736  tdeglem4OLD  26040  amgm  26968  wilthlem2  27046  rpvmasum2  27490  noextendseq  27646  noetasuplem2  27713  noetasuplem4  27715  noetainflem2  27717  noetainflem4  27719  axlowdimlem7  28831  axlowdimlem8  28832  axlowdimlem9  28833  axlowdimlem10  28834  axlowdimlem11  28835  axlowdimlem12  28836  unidifsnne  32411  iundisj2f  32459  fressupp  32550  padct  32583  resf1o  32594  iundisj2fi  32647  fprodeq02  32671  gsummptres2  32857  cycpmconjslem2  32968  cyc3conja  32970  elrspunidl  33240  lbsdiflsp0  33455  dimkerim  33456  locfinref  33573  esummono  33804  esumpad  33805  gsumesum  33809  ldgenpisyslem1  33913  measvuni  33964  pmeasmono  34075  eulerpartlemt  34122  tgoldbachgtde  34423  satfv1lem  35103  fullfunfnv  35673  fullfunfv  35674  opnbnd  35940  pibt2  37027  poimirlem6  37230  poimirlem7  37231  poimirlem15  37239  poimirlem22  37246  ismblfin  37265  evlselv  41955  fsuppssind  41961  diophrw  42321  diophren  42375  tfsconcatfn  42909  tfsconcatfv1  42910  tfsconcatfv2  42911  sumnnodd  45156  sge0ss  45938  meassle  45989  meaunle  45990  meadif  46005  meaiininclem  46012  disjdifb  48066  seposep  48130  iscnrm3rlem1  48145