Theorem disjdif 4470

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

Syntax hints:   = wceq 1539   ∖ cdif 3944   ∩ cin 3946   ⊆ wss 3947  ∅c0 4321

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-dif 3950  df-in 3954  df-ss 3964  df-nul 4322

This theorem is referenced by:  disjdifr  4471  unvdif  4473  difdifdir  4490  fresaun  6761  fresaunres2  6762  fvsnun2  7182  undifixp  8930  undom  9061  undomOLD  9062  enfixsn  9083  sucdom2OLD  9084  sbthlem7  9091  sbthlem8  9092  fodomr  9130  domss2  9138  mapdom2  9150  sucdom2  9208  phplem2OLD  9220  pssnnOLD  9267  dif1ennnALT  9279  unfiOLD  9315  marypha1lem  9430  brwdom2  9570  infdifsn  9654  ackbij1lem12  10228  ssfin4  10307  hashinf  14299  hashfxnn0  14301  hashun2  14347  hashun3  14348  hashssdif  14376  hashfun  14401  hashf1lem2  14421  fsumless  15746  cvgcmpce  15768  incexclem  15786  incexc  15787  fprodsplit1f  15938  mreexexlem3d  17594  sylow2a  19528  gsumval3a  19812  dprd2da  19953  dpjcntz  19963  dpjdisj  19964  dpjlsm  19965  dpjidcl  19969  ablfac1eu  19984  pwssplit1  20814  frlmsslss2  21549  frlmssuvc1  21568  mdetdiaglem  22320  mdetrlin  22324  mdetrsca  22325  mdetralt  22330  smadiadet  22392  nrmsep  23081  dfconn2  23143  fbncp  23563  filufint  23644  supnfcls  23744  flimfnfcls  23752  xrge0gsumle  24569  iundisj2  25298  volsup  25305  itg2cnlem2  25512  tdeglem4OLD  25813  amgm  26731  wilthlem2  26809  rpvmasum2  27251  noextendseq  27406  noetasuplem2  27473  noetasuplem4  27475  noetainflem2  27477  noetainflem4  27479  axlowdimlem7  28473  axlowdimlem8  28474  axlowdimlem9  28475  axlowdimlem10  28476  axlowdimlem11  28477  axlowdimlem12  28478  unidifsnne  32040  iundisj2f  32088  fressupp  32177  padct  32211  resf1o  32222  iundisj2fi  32275  fprodeq02  32296  gsummptres2  32475  cycpmconjslem2  32584  cyc3conja  32586  elrspunidl  32820  lbsdiflsp0  32999  dimkerim  33000  locfinref  33119  esummono  33350  esumpad  33351  gsumesum  33355  ldgenpisyslem1  33459  measvuni  33510  pmeasmono  33621  eulerpartlemt  33668  tgoldbachgtde  33970  satfv1lem  34651  fullfunfnv  35222  fullfunfv  35223  opnbnd  35513  pibt2  36601  poimirlem6  36797  poimirlem7  36798  poimirlem15  36806  poimirlem22  36813  ismblfin  36832  evlselv  41461  fsuppssind  41467  diophrw  41799  diophren  41853  tfsconcatfn  42390  tfsconcatfv1  42391  tfsconcatfv2  42392  sumnnodd  44644  sge0ss  45426  meassle  45477  meaunle  45478  meadif  45493  meaiininclem  45500  disjdifb  47581  seposep  47645  iscnrm3rlem1  47660