Theorem disjdif 4413

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-in 3897  df-ss 3907  df-nul 4275

This theorem is referenced by:  disjdifr  4414  unvdif  4416  difdifdir  4432  fresaun  6705  fresaunres2  6706  fvsnun2  7131  undifixp  8875  undom  8996  enfixsn  9017  sbthlem7  9024  sbthlem8  9025  fodomr  9059  domss2  9067  mapdom2  9079  sucdom2  9130  dif1ennnALT  9180  fodomfir  9231  marypha1lem  9339  brwdom2  9481  infdifsn  9569  ackbij1lem12  10143  ssfin4  10223  hashinf  14288  hashfxnn0  14290  hashun2  14336  hashun3  14337  hashssdif  14365  hashfun  14390  hashf1lem2  14409  fsumless  15750  cvgcmpce  15772  incexclem  15792  incexc  15793  fprodsplit1f  15946  mreexexlem3d  17603  sylow2a  19585  gsumval3a  19869  dprd2da  20010  dpjcntz  20020  dpjdisj  20021  dpjlsm  20022  dpjidcl  20026  ablfac1eu  20041  pwssplit1  21046  frlmsslss2  21765  frlmssuvc1  21784  psdmul  22142  mdetdiaglem  22573  mdetrlin  22577  mdetrsca  22578  mdetralt  22583  smadiadet  22645  nrmsep  23332  dfconn2  23394  fbncp  23814  filufint  23895  supnfcls  23995  flimfnfcls  24003  xrge0gsumle  24809  iundisj2  25526  volsup  25533  itg2cnlem2  25739  amgm  26968  wilthlem2  27046  rpvmasum2  27489  noextendseq  27645  noetasuplem2  27712  noetasuplem4  27714  noetainflem2  27716  noetainflem4  27718  axlowdimlem7  29031  axlowdimlem8  29032  axlowdimlem9  29033  axlowdimlem10  29034  axlowdimlem11  29035  axlowdimlem12  29036  unidifsnne  32621  iundisj2f  32675  fressupp  32776  padct  32806  resf1o  32818  iundisj2fi  32885  fprodeq02  32912  gsummptres2  33129  cycpmconjslem2  33231  cyc3conja  33233  gsumind  33420  elrspunidl  33503  lbsdiflsp0  33786  dimkerim  33787  locfinref  34001  esummono  34214  esumpad  34215  gsumesum  34219  ldgenpisyslem1  34323  measvuni  34374  pmeasmono  34484  eulerpartlemt  34531  tgoldbachgtde  34820  satfv1lem  35560  fullfunfnv  36144  fullfunfv  36145  opnbnd  36523  pibt2  37747  poimirlem6  37961  poimirlem7  37962  poimirlem15  37970  poimirlem22  37977  ismblfin  37996  evlselv  43034  fsuppssind  43040  diophrw  43205  diophren  43259  tfsconcatfn  43784  tfsconcatfv1  43785  tfsconcatfv2  43786  sumnnodd  46078  sge0ss  46858  meassle  46909  meaunle  46910  meadif  46925  meaiininclem  46932  disjdifb  49297  seposep  49413  iscnrm3rlem1  49427