Theorem disjdif 4412

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

Syntax hints:   = wceq 1542   ∖ cdif 3886   ∩ cin 3888   ⊆ wss 3889  ∅c0 4273

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-in 3896  df-ss 3906  df-nul 4274

This theorem is referenced by:  disjdifr  4413  unvdif  4415  difdifdir  4431  fresaun  6711  fresaunres2  6712  fvsnun2  7138  undifixp  8882  undom  9003  enfixsn  9024  sbthlem7  9031  sbthlem8  9032  fodomr  9066  domss2  9074  mapdom2  9086  sucdom2  9137  dif1ennnALT  9187  fodomfir  9238  marypha1lem  9346  brwdom2  9488  infdifsn  9578  ackbij1lem12  10152  ssfin4  10232  hashinf  14297  hashfxnn0  14299  hashun2  14345  hashun3  14346  hashssdif  14374  hashfun  14399  hashf1lem2  14418  fsumless  15759  cvgcmpce  15781  incexclem  15801  incexc  15802  fprodsplit1f  15955  mreexexlem3d  17612  sylow2a  19594  gsumval3a  19878  dprd2da  20019  dpjcntz  20029  dpjdisj  20030  dpjlsm  20031  dpjidcl  20035  ablfac1eu  20050  pwssplit1  21054  frlmsslss2  21755  frlmssuvc1  21774  psdmul  22132  mdetdiaglem  22563  mdetrlin  22567  mdetrsca  22568  mdetralt  22573  smadiadet  22635  nrmsep  23322  dfconn2  23384  fbncp  23804  filufint  23885  supnfcls  23985  flimfnfcls  23993  xrge0gsumle  24799  iundisj2  25516  volsup  25523  itg2cnlem2  25729  amgm  26954  wilthlem2  27032  rpvmasum2  27475  noextendseq  27631  noetasuplem2  27698  noetasuplem4  27700  noetainflem2  27702  noetainflem4  27704  axlowdimlem7  29017  axlowdimlem8  29018  axlowdimlem9  29019  axlowdimlem10  29020  axlowdimlem11  29021  axlowdimlem12  29022  unidifsnne  32606  iundisj2f  32660  fressupp  32761  padct  32791  resf1o  32803  iundisj2fi  32870  fprodeq02  32897  gsummptres2  33114  cycpmconjslem2  33216  cyc3conja  33218  gsumind  33405  elrspunidl  33488  lbsdiflsp0  33770  dimkerim  33771  locfinref  33985  esummono  34198  esumpad  34199  gsumesum  34203  ldgenpisyslem1  34307  measvuni  34358  pmeasmono  34468  eulerpartlemt  34515  tgoldbachgtde  34804  satfv1lem  35544  fullfunfnv  36128  fullfunfv  36129  opnbnd  36507  pibt2  37733  poimirlem6  37947  poimirlem7  37948  poimirlem15  37956  poimirlem22  37963  ismblfin  37982  evlselv  43020  fsuppssind  43026  diophrw  43191  diophren  43241  tfsconcatfn  43766  tfsconcatfv1  43767  tfsconcatfv2  43768  sumnnodd  46060  sge0ss  46840  meassle  46891  meaunle  46892  meadif  46907  meaiininclem  46914  disjdifb  49285  seposep  49401  iscnrm3rlem1  49415