Theorem disjdif 4429

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

Syntax hints:   = wceq 1563   ∖ cdif 3904   ∩ cin 3906   ⊆ wss 3907  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3910  df-in 3914  df-ss 3924  df-nul 4289

This theorem is referenced by:  disjdifr  4430  unvdif  4432  difdifdir  4448  fresaun  6739  fresaunres2  6740  fvsnun2  7171  undifixp  8920  undom  9041  enfixsn  9062  sbthlem7  9069  sbthlem8  9070  fodomr  9104  domss2  9112  mapdom2  9124  sucdom2  9175  dif1ennnALT  9225  fodomfir  9275  marypha1lem  9381  brwdom2  9523  infdifsn  9614  ackbij1lem12  10201  ssfin4  10282  hashinf  14362  hashfxnn0  14364  hashun2  14410  hashun3  14411  hashssdif  14439  hashfun  14464  hashf1lem2  14483  fsumless  15838  cvgcmpce  15860  incexclem  15880  incexc  15881  fprodsplit1f  16034  mreexexlem3d  17692  sylow2a  19680  gsumval3a  19964  dprd2da  20105  dpjcntz  20115  dpjdisj  20116  dpjlsm  20117  dpjidcl  20121  ablfac1eu  20136  pwssplit1  21149  frlmsslss2  21885  frlmssuvc1  21904  psdmul  22289  mdetdiaglem  22716  mdetrlin  22720  mdetrsca  22721  mdetralt  22726  smadiadet  22788  nrmsep  23475  dfconn2  23537  fbncp  23957  filufint  24038  supnfcls  24138  flimfnfcls  24146  xrge0gsumle  24952  iundisj2  25669  volsup  25676  itg2cnlem2  25882  amgm  27113  wilthlem2  27191  rpvmasum2  27634  noextendseq  27789  noetasuplem2  27856  noetasuplem4  27858  noetainflem2  27860  noetainflem4  27862  axlowdimlem7  29207  axlowdimlem8  29208  axlowdimlem9  29209  axlowdimlem10  29210  axlowdimlem11  29211  axlowdimlem12  29212  unidifsnne  32792  iundisj2f  32845  fressupp  32945  padct  32975  resf1o  32987  iundisj2fi  33054  fprodeq02  33081  gsummptres2  33286  cycpmconjslem2  33388  cyc3conja  33390  gsumind  33580  elrspunidl  33652  lbsdiflsp0  33933  dimkerim  33934  locfinref  34148  esummono  34361  esumpad  34362  gsumesum  34366  ldgenpisyslem1  34470  measvuni  34521  pmeasmono  34631  eulerpartlemt  34678  tgoldbachgtde  34964  satfv1lem  35725  fullfunfnv  36309  fullfunfv  36310  opnbnd  36698  pibt2  37923  poimirlem6  38137  poimirlem7  38138  poimirlem15  38146  poimirlem22  38153  ismblfin  38172  evlselv  43183  fsuppssind  43187  diophrw  43352  diophren  43402  tfsconcatfn  43927  tfsconcatfv1  43928  tfsconcatfv2  43929  sumnnodd  46204  sge0ss  46984  meassle  47035  meaunle  47036  meadif  47051  meaiininclem  47058  disjdifb  49439  seposep  49555  iscnrm3rlem1  49569