Theorem disjdif 4422

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

Syntax hints:   = wceq 1541   ∖ cdif 3899   ∩ cin 3901   ⊆ wss 3902  ∅c0 4283

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-in 3909  df-ss 3919  df-nul 4284

This theorem is referenced by:  disjdifr  4423  unvdif  4425  difdifdir  4442  fresaun  6694  fresaunres2  6695  fvsnun2  7117  undifixp  8858  undom  8978  enfixsn  8999  sbthlem7  9006  sbthlem8  9007  fodomr  9041  domss2  9049  mapdom2  9061  sucdom2  9112  dif1ennnALT  9161  fodomfir  9212  marypha1lem  9317  brwdom2  9459  infdifsn  9547  ackbij1lem12  10118  ssfin4  10198  hashinf  14239  hashfxnn0  14241  hashun2  14287  hashun3  14288  hashssdif  14316  hashfun  14341  hashf1lem2  14360  fsumless  15700  cvgcmpce  15722  incexclem  15740  incexc  15741  fprodsplit1f  15894  mreexexlem3d  17549  sylow2a  19529  gsumval3a  19813  dprd2da  19954  dpjcntz  19964  dpjdisj  19965  dpjlsm  19966  dpjidcl  19970  ablfac1eu  19985  pwssplit1  20991  frlmsslss2  21710  frlmssuvc1  21729  psdmul  22079  mdetdiaglem  22511  mdetrlin  22515  mdetrsca  22516  mdetralt  22521  smadiadet  22583  nrmsep  23270  dfconn2  23332  fbncp  23752  filufint  23833  supnfcls  23933  flimfnfcls  23941  xrge0gsumle  24747  iundisj2  25475  volsup  25482  itg2cnlem2  25688  amgm  26926  wilthlem2  27004  rpvmasum2  27448  noextendseq  27604  noetasuplem2  27671  noetasuplem4  27673  noetainflem2  27675  noetainflem4  27677  axlowdimlem7  28924  axlowdimlem8  28925  axlowdimlem9  28926  axlowdimlem10  28927  axlowdimlem11  28928  axlowdimlem12  28929  unidifsnne  32511  iundisj2f  32565  fressupp  32664  padct  32696  resf1o  32708  iundisj2fi  32774  fprodeq02  32801  gsummptres2  33028  cycpmconjslem2  33119  cyc3conja  33121  gsumind  33305  elrspunidl  33388  lbsdiflsp0  33634  dimkerim  33635  locfinref  33849  esummono  34062  esumpad  34063  gsumesum  34067  ldgenpisyslem1  34171  measvuni  34222  pmeasmono  34332  eulerpartlemt  34379  tgoldbachgtde  34668  satfv1lem  35394  fullfunfnv  35979  fullfunfv  35980  opnbnd  36358  pibt2  37450  poimirlem6  37665  poimirlem7  37666  poimirlem15  37674  poimirlem22  37681  ismblfin  37700  evlselv  42619  fsuppssind  42625  diophrw  42791  diophren  42845  tfsconcatfn  43370  tfsconcatfv1  43371  tfsconcatfv2  43372  sumnnodd  45669  sge0ss  46449  meassle  46500  meaunle  46501  meadif  46516  meaiininclem  46523  disjdifb  48840  seposep  48956  iscnrm3rlem1  48970