Theorem disjdif 4424

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

Syntax hints:   = wceq 1541   ∖ cdif 3898   ∩ cin 3900   ⊆ wss 3901  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-in 3908  df-ss 3918  df-nul 4286

This theorem is referenced by:  disjdifr  4425  unvdif  4427  difdifdir  4444  fresaun  6705  fresaunres2  6706  fvsnun2  7129  undifixp  8872  undom  8993  enfixsn  9014  sbthlem7  9021  sbthlem8  9022  fodomr  9056  domss2  9064  mapdom2  9076  sucdom2  9127  dif1ennnALT  9177  fodomfir  9228  marypha1lem  9336  brwdom2  9478  infdifsn  9566  ackbij1lem12  10140  ssfin4  10220  hashinf  14258  hashfxnn0  14260  hashun2  14306  hashun3  14307  hashssdif  14335  hashfun  14360  hashf1lem2  14379  fsumless  15719  cvgcmpce  15741  incexclem  15759  incexc  15760  fprodsplit1f  15913  mreexexlem3d  17569  sylow2a  19548  gsumval3a  19832  dprd2da  19973  dpjcntz  19983  dpjdisj  19984  dpjlsm  19985  dpjidcl  19989  ablfac1eu  20004  pwssplit1  21011  frlmsslss2  21730  frlmssuvc1  21749  psdmul  22109  mdetdiaglem  22542  mdetrlin  22546  mdetrsca  22547  mdetralt  22552  smadiadet  22614  nrmsep  23301  dfconn2  23363  fbncp  23783  filufint  23864  supnfcls  23964  flimfnfcls  23972  xrge0gsumle  24778  iundisj2  25506  volsup  25513  itg2cnlem2  25719  amgm  26957  wilthlem2  27035  rpvmasum2  27479  noextendseq  27635  noetasuplem2  27702  noetasuplem4  27704  noetainflem2  27706  noetainflem4  27708  axlowdimlem7  29021  axlowdimlem8  29022  axlowdimlem9  29023  axlowdimlem10  29024  axlowdimlem11  29025  axlowdimlem12  29026  unidifsnne  32611  iundisj2f  32665  fressupp  32767  padct  32797  resf1o  32809  iundisj2fi  32877  fprodeq02  32904  gsummptres2  33136  cycpmconjslem2  33237  cyc3conja  33239  gsumind  33426  elrspunidl  33509  lbsdiflsp0  33783  dimkerim  33784  locfinref  33998  esummono  34211  esumpad  34212  gsumesum  34216  ldgenpisyslem1  34320  measvuni  34371  pmeasmono  34481  eulerpartlemt  34528  tgoldbachgtde  34817  satfv1lem  35556  fullfunfnv  36140  fullfunfv  36141  opnbnd  36519  pibt2  37618  poimirlem6  37823  poimirlem7  37824  poimirlem15  37832  poimirlem22  37839  ismblfin  37858  evlselv  42826  fsuppssind  42832  diophrw  42997  diophren  43051  tfsconcatfn  43576  tfsconcatfv1  43577  tfsconcatfv2  43578  sumnnodd  45872  sge0ss  46652  meassle  46703  meaunle  46704  meadif  46719  meaiininclem  46726  disjdifb  49051  seposep  49167  iscnrm3rlem1  49181