Theorem disjdif 4452

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

Syntax hints:   = wceq 1540   ∖ cdif 3928   ∩ cin 3930   ⊆ wss 3931  ∅c0 4313

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 2008  ax-8 2111  ax-9 2119  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 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934  df-in 3938  df-ss 3948  df-nul 4314

This theorem is referenced by:  disjdifr  4453  unvdif  4455  difdifdir  4472  fresaun  6754  fresaunres2  6755  fvsnun2  7180  undifixp  8953  undom  9078  undomOLD  9079  enfixsn  9100  sucdom2OLD  9101  sbthlem7  9108  sbthlem8  9109  fodomr  9147  domss2  9155  mapdom2  9167  sucdom2  9222  phplem2OLD  9234  dif1ennnALT  9288  fodomfir  9345  marypha1lem  9450  brwdom2  9592  infdifsn  9676  ackbij1lem12  10249  ssfin4  10329  hashinf  14358  hashfxnn0  14360  hashun2  14406  hashun3  14407  hashssdif  14435  hashfun  14460  hashf1lem2  14479  fsumless  15817  cvgcmpce  15839  incexclem  15857  incexc  15858  fprodsplit1f  16011  mreexexlem3d  17663  sylow2a  19605  gsumval3a  19889  dprd2da  20030  dpjcntz  20040  dpjdisj  20041  dpjlsm  20042  dpjidcl  20046  ablfac1eu  20061  pwssplit1  21022  frlmsslss2  21740  frlmssuvc1  21759  psdmul  22109  mdetdiaglem  22541  mdetrlin  22545  mdetrsca  22546  mdetralt  22551  smadiadet  22613  nrmsep  23300  dfconn2  23362  fbncp  23782  filufint  23863  supnfcls  23963  flimfnfcls  23971  xrge0gsumle  24778  iundisj2  25507  volsup  25514  itg2cnlem2  25720  amgm  26958  wilthlem2  27036  rpvmasum2  27480  noextendseq  27636  noetasuplem2  27703  noetasuplem4  27705  noetainflem2  27707  noetainflem4  27709  axlowdimlem7  28932  axlowdimlem8  28933  axlowdimlem9  28934  axlowdimlem10  28935  axlowdimlem11  28936  axlowdimlem12  28937  unidifsnne  32522  iundisj2f  32576  fressupp  32670  padct  32702  resf1o  32712  iundisj2fi  32779  fprodeq02  32807  gsummptres2  33052  cycpmconjslem2  33171  cyc3conja  33173  elrspunidl  33448  lbsdiflsp0  33671  dimkerim  33672  locfinref  33877  esummono  34090  esumpad  34091  gsumesum  34095  ldgenpisyslem1  34199  measvuni  34250  pmeasmono  34361  eulerpartlemt  34408  tgoldbachgtde  34697  satfv1lem  35389  fullfunfnv  35969  fullfunfv  35970  opnbnd  36348  pibt2  37440  poimirlem6  37655  poimirlem7  37656  poimirlem15  37664  poimirlem22  37671  ismblfin  37690  evlselv  42585  fsuppssind  42591  diophrw  42757  diophren  42811  tfsconcatfn  43337  tfsconcatfv1  43338  tfsconcatfv2  43339  sumnnodd  45639  sge0ss  46421  meassle  46472  meaunle  46473  meadif  46488  meaiininclem  46495  disjdifb  48768  seposep  48880  iscnrm3rlem1  48894