Theorem disjdif 4426

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

Syntax hints:   = wceq 1542   ∖ cdif 3900   ∩ cin 3902   ⊆ wss 3903  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-in 3910  df-ss 3920  df-nul 4288

This theorem is referenced by:  disjdifr  4427  unvdif  4429  difdifdir  4446  fresaun  6713  fresaunres2  6714  fvsnun2  7139  undifixp  8884  undom  9005  enfixsn  9026  sbthlem7  9033  sbthlem8  9034  fodomr  9068  domss2  9076  mapdom2  9088  sucdom2  9139  dif1ennnALT  9189  fodomfir  9240  marypha1lem  9348  brwdom2  9490  infdifsn  9578  ackbij1lem12  10152  ssfin4  10232  hashinf  14270  hashfxnn0  14272  hashun2  14318  hashun3  14319  hashssdif  14347  hashfun  14372  hashf1lem2  14391  fsumless  15731  cvgcmpce  15753  incexclem  15771  incexc  15772  fprodsplit1f  15925  mreexexlem3d  17581  sylow2a  19560  gsumval3a  19844  dprd2da  19985  dpjcntz  19995  dpjdisj  19996  dpjlsm  19997  dpjidcl  20001  ablfac1eu  20016  pwssplit1  21023  frlmsslss2  21742  frlmssuvc1  21761  psdmul  22121  mdetdiaglem  22554  mdetrlin  22558  mdetrsca  22559  mdetralt  22564  smadiadet  22626  nrmsep  23313  dfconn2  23375  fbncp  23795  filufint  23876  supnfcls  23976  flimfnfcls  23984  xrge0gsumle  24790  iundisj2  25518  volsup  25525  itg2cnlem2  25731  amgm  26969  wilthlem2  27047  rpvmasum2  27491  noextendseq  27647  noetasuplem2  27714  noetasuplem4  27716  noetainflem2  27718  noetainflem4  27720  axlowdimlem7  29033  axlowdimlem8  29034  axlowdimlem9  29035  axlowdimlem10  29036  axlowdimlem11  29037  axlowdimlem12  29038  unidifsnne  32622  iundisj2f  32676  fressupp  32777  padct  32807  resf1o  32819  iundisj2fi  32887  fprodeq02  32914  gsummptres2  33146  cycpmconjslem2  33248  cyc3conja  33250  gsumind  33437  elrspunidl  33520  lbsdiflsp0  33803  dimkerim  33804  locfinref  34018  esummono  34231  esumpad  34232  gsumesum  34236  ldgenpisyslem1  34340  measvuni  34391  pmeasmono  34501  eulerpartlemt  34548  tgoldbachgtde  34837  satfv1lem  35575  fullfunfnv  36159  fullfunfv  36160  opnbnd  36538  pibt2  37666  poimirlem6  37871  poimirlem7  37872  poimirlem15  37880  poimirlem22  37887  ismblfin  37906  evlselv  42939  fsuppssind  42945  diophrw  43110  diophren  43164  tfsconcatfn  43689  tfsconcatfv1  43690  tfsconcatfv2  43691  sumnnodd  45984  sge0ss  46764  meassle  46815  meaunle  46816  meadif  46831  meaiininclem  46838  disjdifb  49163  seposep  49279  iscnrm3rlem1  49293