Theorem disjdif 4407

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

Syntax hints:   = wceq 1547   ∖ cdif 3887   ∩ cin 3889   ⊆ wss 3890  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-dif 3893  df-in 3897  df-ss 3907  df-nul 4269

This theorem is referenced by:  disjdifr  4408  unvdif  4410  difdifdir  4426  fresaun  6705  fresaunres2  6706  fvsnun2  7134  undifixp  8879  undom  9000  enfixsn  9021  sbthlem7  9028  sbthlem8  9029  fodomr  9063  domss2  9071  mapdom2  9083  sucdom2  9134  dif1ennnALT  9184  fodomfir  9235  marypha1lem  9343  brwdom2  9485  infdifsn  9576  ackbij1lem12  10150  ssfin4  10230  hashinf  14295  hashfxnn0  14297  hashun2  14343  hashun3  14344  hashssdif  14372  hashfun  14397  hashf1lem2  14416  fsumless  15757  cvgcmpce  15779  incexclem  15799  incexc  15800  fprodsplit1f  15953  mreexexlem3d  17610  sylow2a  19592  gsumval3a  19876  dprd2da  20017  dpjcntz  20027  dpjdisj  20028  dpjlsm  20029  dpjidcl  20033  ablfac1eu  20048  pwssplit1  21056  frlmsslss2  21757  frlmssuvc1  21776  psdmul  22161  mdetdiaglem  22588  mdetrlin  22592  mdetrsca  22593  mdetralt  22598  smadiadet  22660  nrmsep  23347  dfconn2  23409  fbncp  23829  filufint  23910  supnfcls  24010  flimfnfcls  24018  xrge0gsumle  24824  iundisj2  25541  volsup  25548  itg2cnlem2  25754  amgm  26979  wilthlem2  27057  rpvmasum2  27500  noextendseq  27656  noetasuplem2  27723  noetasuplem4  27725  noetainflem2  27727  noetainflem4  27729  axlowdimlem7  29042  axlowdimlem8  29043  axlowdimlem9  29044  axlowdimlem10  29045  axlowdimlem11  29046  axlowdimlem12  29047  unidifsnne  32631  iundisj2f  32686  fressupp  32787  padct  32817  resf1o  32829  iundisj2fi  32896  fprodeq02  32923  gsummptres2  33141  cycpmconjslem2  33243  cyc3conja  33245  gsumind  33435  elrspunidl  33518  lbsdiflsp0  33817  dimkerim  33818  locfinref  34032  esummono  34245  esumpad  34246  gsumesum  34250  ldgenpisyslem1  34354  measvuni  34405  pmeasmono  34515  eulerpartlemt  34562  tgoldbachgtde  34851  satfv1lem  35597  fullfunfnv  36181  fullfunfv  36182  opnbnd  36560  pibt2  37786  poimirlem6  38000  poimirlem7  38001  poimirlem15  38009  poimirlem22  38016  ismblfin  38035  evlselv  43046  fsuppssind  43050  diophrw  43215  diophren  43265  tfsconcatfn  43790  tfsconcatfv1  43791  tfsconcatfv2  43792  sumnnodd  46082  sge0ss  46862  meassle  46913  meaunle  46914  meadif  46929  meaiininclem  46936  disjdifb  49307  seposep  49423  iscnrm3rlem1  49437