Theorem disjdif 4421

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

Syntax hints:   = wceq 1537   ∖ cdif 3933   ∩ cin 3935   ⊆ wss 3936  ∅c0 4291

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-in 3943  df-ss 3952  df-nul 4292

This theorem is referenced by:  unvdif  4423  ssdifin0  4431  difdifdir  4437  fresaun  6549  fresaunres2  6550  fvsnun1  6944  fvsnun2  6945  fveqf1o  7058  ralxpmap  8460  undifixp  8498  difsnen  8599  undom  8605  enfixsn  8626  sbthlem7  8633  sbthlem8  8634  domunsn  8667  fodomr  8668  domss2  8676  mapdom2  8688  limensuci  8693  phplem2  8697  sucdom2  8714  pssnn  8736  dif1en  8751  unfi  8785  marypha1lem  8897  brwdom2  9037  infdifsn  9120  dif1card  9436  ackbij1lem12  9653  ackbij1lem18  9659  ssfin4  9732  canthp1lem1  10074  grothprim  10256  hashgval  13694  hashinf  13696  hashfxnn0  13698  hashun2  13745  hashun3  13746  hashssdif  13774  hashfun  13799  hashbclem  13811  hashf1lem2  13815  fsumless  15151  cvgcmpce  15173  incexclem  15191  incexc  15192  fprodsplit1f  15344  setsfun  16518  setsfun0  16519  setsid  16538  mreexexlem3d  16917  mreexexlem4d  16918  sylow2a  18744  gsumval3a  19023  dprd2da  19164  dpjcntz  19174  dpjdisj  19175  dpjlsm  19176  dpjidcl  19180  ablfac1eu  19195  pwssplit1  19831  frlmsslss2  20919  frlmssuvc1  20938  frlmsslsp  20940  islindf4  20982  mdetdiaglem  21207  mdetrlin  21211  mdetrsca  21212  mdetralt  21217  smadiadet  21279  neitr  21788  nrmsep  21965  regsep2  21984  dfconn2  22027  fbncp  22447  filufint  22528  supnfcls  22628  flimfnfcls  22636  restmetu  23180  xrge0gsumle  23441  volinun  24147  iundisj2  24150  volsup  24157  itg2cnlem2  24363  tdeglem4  24654  amgm  25568  wilthlem2  25646  rpvmasum2  26088  axlowdimlem7  26734  axlowdimlem8  26735  axlowdimlem9  26736  axlowdimlem10  26737  axlowdimlem11  26738  axlowdimlem12  26739  disjdifr  30275  difeq  30280  unidifsnne  30296  disjdifprg  30325  iundisj2f  30340  padct  30455  resf1o  30466  iundisj2fi  30520  fprodeq02  30539  tocycfvres1  30752  tocycfvres2  30753  cycpmfvlem  30754  cycpmfv3  30757  cycpmcl  30758  cycpmconjslem2  30797  cyc3conja  30799  lbsdiflsp0  31022  dimkerim  31023  locfinref  31105  esummono  31313  esumpad  31314  gsumesum  31318  ldgenpisyslem1  31422  measvuni  31473  measunl  31475  pmeasmono  31582  eulerpartlemt  31629  tgoldbachgtde  31931  satfv1lem  32609  mthmpps  32829  noextendseq  33174  noetalem2  33218  noetalem3  33219  fullfunfnv  33407  fullfunfv  33408  opnbnd  33673  cldbnd  33674  pibt2  34701  poimirlem6  34913  poimirlem7  34914  poimirlem15  34922  poimirlem16  34923  poimirlem19  34926  poimirlem22  34929  poimirlem27  34934  ismblfin  34948  diophrw  39376  eldioph2lem1  39377  eldioph2lem2  39378  diophren  39430  kelac1  39683  sumnnodd  41931  sge0ss  42714  meassle  42765  meaunle  42766  meadif  42781  meaiininclem  42788  isomenndlem  42832