Theorem disjdif 4472

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

Syntax hints:   = wceq 1540   ∖ cdif 3948   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-in 3958  df-ss 3968  df-nul 4334

This theorem is referenced by:  disjdifr  4473  unvdif  4475  difdifdir  4492  fresaun  6779  fresaunres2  6780  fvsnun2  7203  undifixp  8974  undom  9099  undomOLD  9100  enfixsn  9121  sucdom2OLD  9122  sbthlem7  9129  sbthlem8  9130  fodomr  9168  domss2  9176  mapdom2  9188  sucdom2  9243  phplem2OLD  9255  dif1ennnALT  9311  fodomfir  9368  marypha1lem  9473  brwdom2  9613  infdifsn  9697  ackbij1lem12  10270  ssfin4  10350  hashinf  14374  hashfxnn0  14376  hashun2  14422  hashun3  14423  hashssdif  14451  hashfun  14476  hashf1lem2  14495  fsumless  15832  cvgcmpce  15854  incexclem  15872  incexc  15873  fprodsplit1f  16026  mreexexlem3d  17689  sylow2a  19637  gsumval3a  19921  dprd2da  20062  dpjcntz  20072  dpjdisj  20073  dpjlsm  20074  dpjidcl  20078  ablfac1eu  20093  pwssplit1  21058  frlmsslss2  21795  frlmssuvc1  21814  psdmul  22170  mdetdiaglem  22604  mdetrlin  22608  mdetrsca  22609  mdetralt  22614  smadiadet  22676  nrmsep  23365  dfconn2  23427  fbncp  23847  filufint  23928  supnfcls  24028  flimfnfcls  24036  xrge0gsumle  24855  iundisj2  25584  volsup  25591  itg2cnlem2  25797  amgm  27034  wilthlem2  27112  rpvmasum2  27556  noextendseq  27712  noetasuplem2  27779  noetasuplem4  27781  noetainflem2  27783  noetainflem4  27785  axlowdimlem7  28963  axlowdimlem8  28964  axlowdimlem9  28965  axlowdimlem10  28966  axlowdimlem11  28967  axlowdimlem12  28968  unidifsnne  32554  iundisj2f  32603  fressupp  32697  padct  32731  resf1o  32741  iundisj2fi  32799  fprodeq02  32825  gsummptres2  33056  cycpmconjslem2  33175  cyc3conja  33177  elrspunidl  33456  lbsdiflsp0  33677  dimkerim  33678  locfinref  33840  esummono  34055  esumpad  34056  gsumesum  34060  ldgenpisyslem1  34164  measvuni  34215  pmeasmono  34326  eulerpartlemt  34373  tgoldbachgtde  34675  satfv1lem  35367  fullfunfnv  35947  fullfunfv  35948  opnbnd  36326  pibt2  37418  poimirlem6  37633  poimirlem7  37634  poimirlem15  37642  poimirlem22  37649  ismblfin  37668  evlselv  42597  fsuppssind  42603  diophrw  42770  diophren  42824  tfsconcatfn  43351  tfsconcatfv1  43352  tfsconcatfv2  43353  sumnnodd  45645  sge0ss  46427  meassle  46478  meaunle  46479  meadif  46494  meaiininclem  46501  disjdifb  48729  seposep  48823  iscnrm3rlem1  48837