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

Syntax hints:   = wceq 1541   ∖ cdif 3895   ∩ cin 3897   ⊆ wss 3898  ∅c0 4282

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-in 3905  df-ss 3915  df-nul 4283

This theorem is referenced by:  disjdifr  4422  unvdif  4424  difdifdir  4441  fresaun  6699  fresaunres2  6700  fvsnun2  7123  undifixp  8864  undom  8985  enfixsn  9006  sbthlem7  9013  sbthlem8  9014  fodomr  9048  domss2  9056  mapdom2  9068  sucdom2  9119  dif1ennnALT  9168  fodomfir  9219  marypha1lem  9324  brwdom2  9466  infdifsn  9554  ackbij1lem12  10128  ssfin4  10208  hashinf  14244  hashfxnn0  14246  hashun2  14292  hashun3  14293  hashssdif  14321  hashfun  14346  hashf1lem2  14365  fsumless  15705  cvgcmpce  15727  incexclem  15745  incexc  15746  fprodsplit1f  15899  mreexexlem3d  17554  sylow2a  19533  gsumval3a  19817  dprd2da  19958  dpjcntz  19968  dpjdisj  19969  dpjlsm  19970  dpjidcl  19974  ablfac1eu  19989  pwssplit1  20995  frlmsslss2  21714  frlmssuvc1  21733  psdmul  22082  mdetdiaglem  22514  mdetrlin  22518  mdetrsca  22519  mdetralt  22524  smadiadet  22586  nrmsep  23273  dfconn2  23335  fbncp  23755  filufint  23836  supnfcls  23936  flimfnfcls  23944  xrge0gsumle  24750  iundisj2  25478  volsup  25485  itg2cnlem2  25691  amgm  26929  wilthlem2  27007  rpvmasum2  27451  noextendseq  27607  noetasuplem2  27674  noetasuplem4  27676  noetainflem2  27678  noetainflem4  27680  axlowdimlem7  28928  axlowdimlem8  28929  axlowdimlem9  28930  axlowdimlem10  28931  axlowdimlem11  28932  axlowdimlem12  28933  unidifsnne  32518  iundisj2f  32572  fressupp  32673  padct  32705  resf1o  32717  iundisj2fi  32784  fprodeq02  32811  gsummptres2  33040  cycpmconjslem2  33131  cyc3conja  33133  gsumind  33317  elrspunidl  33400  lbsdiflsp0  33660  dimkerim  33661  locfinref  33875  esummono  34088  esumpad  34089  gsumesum  34093  ldgenpisyslem1  34197  measvuni  34248  pmeasmono  34358  eulerpartlemt  34405  tgoldbachgtde  34694  satfv1lem  35427  fullfunfnv  36011  fullfunfv  36012  opnbnd  36390  pibt2  37482  poimirlem6  37686  poimirlem7  37687  poimirlem15  37695  poimirlem22  37702  ismblfin  37721  evlselv  42705  fsuppssind  42711  diophrw  42876  diophren  42930  tfsconcatfn  43455  tfsconcatfv1  43456  tfsconcatfv2  43457  sumnnodd  45754  sge0ss  46534  meassle  46585  meaunle  46586  meadif  46601  meaiininclem  46608  disjdifb  48934  seposep  49050  iscnrm3rlem1  49064