Theorem disjdif 4425

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

Syntax hints:   = wceq 1540   ∖ cdif 3902   ∩ cin 3904   ⊆ wss 3905  ∅c0 4286

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-in 3912  df-ss 3922  df-nul 4287

This theorem is referenced by:  disjdifr  4426  unvdif  4428  difdifdir  4445  fresaun  6699  fresaunres2  6700  fvsnun2  7123  undifixp  8868  undom  8989  enfixsn  9010  sbthlem7  9017  sbthlem8  9018  fodomr  9052  domss2  9060  mapdom2  9072  sucdom2  9127  dif1ennnALT  9180  fodomfir  9237  marypha1lem  9342  brwdom2  9484  infdifsn  9572  ackbij1lem12  10143  ssfin4  10223  hashinf  14260  hashfxnn0  14262  hashun2  14308  hashun3  14309  hashssdif  14337  hashfun  14362  hashf1lem2  14381  fsumless  15721  cvgcmpce  15743  incexclem  15761  incexc  15762  fprodsplit1f  15915  mreexexlem3d  17570  sylow2a  19516  gsumval3a  19800  dprd2da  19941  dpjcntz  19951  dpjdisj  19952  dpjlsm  19953  dpjidcl  19957  ablfac1eu  19972  pwssplit1  20981  frlmsslss2  21700  frlmssuvc1  21719  psdmul  22069  mdetdiaglem  22501  mdetrlin  22505  mdetrsca  22506  mdetralt  22511  smadiadet  22573  nrmsep  23260  dfconn2  23322  fbncp  23742  filufint  23823  supnfcls  23923  flimfnfcls  23931  xrge0gsumle  24738  iundisj2  25466  volsup  25473  itg2cnlem2  25679  amgm  26917  wilthlem2  26995  rpvmasum2  27439  noextendseq  27595  noetasuplem2  27662  noetasuplem4  27664  noetainflem2  27666  noetainflem4  27668  axlowdimlem7  28911  axlowdimlem8  28912  axlowdimlem9  28913  axlowdimlem10  28914  axlowdimlem11  28915  axlowdimlem12  28916  unidifsnne  32498  iundisj2f  32552  fressupp  32644  padct  32676  resf1o  32686  iundisj2fi  32753  fprodeq02  32781  gsummptres2  33019  cycpmconjslem2  33110  cyc3conja  33112  elrspunidl  33375  lbsdiflsp0  33598  dimkerim  33599  locfinref  33807  esummono  34020  esumpad  34021  gsumesum  34025  ldgenpisyslem1  34129  measvuni  34180  pmeasmono  34291  eulerpartlemt  34338  tgoldbachgtde  34627  satfv1lem  35334  fullfunfnv  35919  fullfunfv  35920  opnbnd  36298  pibt2  37390  poimirlem6  37605  poimirlem7  37606  poimirlem15  37614  poimirlem22  37621  ismblfin  37640  evlselv  42560  fsuppssind  42566  diophrw  42732  diophren  42786  tfsconcatfn  43311  tfsconcatfv1  43312  tfsconcatfv2  43313  sumnnodd  45612  sge0ss  46394  meassle  46445  meaunle  46446  meadif  46461  meaiininclem  46468  disjdifb  48795  seposep  48911  iscnrm3rlem1  48925