Theorem disjdif 4402

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

Syntax hints:   = wceq 1539   ∖ cdif 3880   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900  df-nul 4254

This theorem is referenced by:  disjdifr  4403  unvdif  4405  difdifdir  4419  fresaun  6629  fresaunres2  6630  fvsnun2  7037  undifixp  8680  undom  8800  enfixsn  8821  sucdom2  8822  sbthlem7  8829  sbthlem8  8830  fodomr  8864  domss2  8872  mapdom2  8884  phplem2  8893  pssnnOLD  8969  dif1enALT  8980  unfiOLD  9011  marypha1lem  9122  brwdom2  9262  infdifsn  9345  ackbij1lem12  9918  ssfin4  9997  hashinf  13977  hashfxnn0  13979  hashun2  14026  hashun3  14027  hashssdif  14055  hashfun  14080  hashf1lem2  14098  fsumless  15436  cvgcmpce  15458  incexclem  15476  incexc  15477  fprodsplit1f  15628  mreexexlem3d  17272  sylow2a  19139  gsumval3a  19419  dprd2da  19560  dpjcntz  19570  dpjdisj  19571  dpjlsm  19572  dpjidcl  19576  ablfac1eu  19591  pwssplit1  20236  frlmsslss2  20892  frlmssuvc1  20911  mdetdiaglem  21655  mdetrlin  21659  mdetrsca  21660  mdetralt  21665  smadiadet  21727  nrmsep  22416  dfconn2  22478  fbncp  22898  filufint  22979  supnfcls  23079  flimfnfcls  23087  xrge0gsumle  23902  iundisj2  24618  volsup  24625  itg2cnlem2  24832  tdeglem4OLD  25130  amgm  26045  wilthlem2  26123  rpvmasum2  26565  axlowdimlem7  27219  axlowdimlem8  27220  axlowdimlem9  27221  axlowdimlem10  27222  axlowdimlem11  27223  axlowdimlem12  27224  unidifsnne  30785  iundisj2f  30830  fressupp  30924  padct  30956  resf1o  30967  iundisj2fi  31020  fprodeq02  31039  gsummptres2  31215  cycpmconjslem2  31324  cyc3conja  31326  elrspunidl  31508  lbsdiflsp0  31609  dimkerim  31610  locfinref  31693  esummono  31922  esumpad  31923  gsumesum  31927  ldgenpisyslem1  32031  measvuni  32082  pmeasmono  32191  eulerpartlemt  32238  tgoldbachgtde  32540  satfv1lem  33224  noextendseq  33797  noetasuplem2  33864  noetasuplem4  33866  noetainflem2  33868  noetainflem4  33870  fullfunfnv  34175  fullfunfv  34176  opnbnd  34441  pibt2  35515  poimirlem6  35710  poimirlem7  35711  poimirlem15  35719  poimirlem22  35726  ismblfin  35745  fsuppssind  40205  diophrw  40497  diophren  40551  sumnnodd  43061  sge0ss  43840  meassle  43891  meaunle  43892  meadif  43907  meaiininclem  43914  disjdifb  46043  seposep  46107  iscnrm3rlem1  46122