Theorem disjdif 4477

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

Syntax hints:   = wceq 1536   ∖ cdif 3959   ∩ cin 3961   ⊆ wss 3962  ∅c0 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-in 3969  df-ss 3979  df-nul 4339

This theorem is referenced by:  disjdifr  4478  unvdif  4480  difdifdir  4497  fresaun  6779  fresaunres2  6780  fvsnun2  7202  undifixp  8972  undom  9097  undomOLD  9098  enfixsn  9119  sucdom2OLD  9120  sbthlem7  9127  sbthlem8  9128  fodomr  9166  domss2  9174  mapdom2  9186  sucdom2  9240  phplem2OLD  9252  dif1ennnALT  9308  fodomfir  9365  marypha1lem  9470  brwdom2  9610  infdifsn  9694  ackbij1lem12  10267  ssfin4  10347  hashinf  14370  hashfxnn0  14372  hashun2  14418  hashun3  14419  hashssdif  14447  hashfun  14472  hashf1lem2  14491  fsumless  15828  cvgcmpce  15850  incexclem  15868  incexc  15869  fprodsplit1f  16022  mreexexlem3d  17690  sylow2a  19651  gsumval3a  19935  dprd2da  20076  dpjcntz  20086  dpjdisj  20087  dpjlsm  20088  dpjidcl  20092  ablfac1eu  20107  pwssplit1  21075  frlmsslss2  21812  frlmssuvc1  21831  psdmul  22187  mdetdiaglem  22619  mdetrlin  22623  mdetrsca  22624  mdetralt  22629  smadiadet  22691  nrmsep  23380  dfconn2  23442  fbncp  23862  filufint  23943  supnfcls  24043  flimfnfcls  24051  xrge0gsumle  24868  iundisj2  25597  volsup  25604  itg2cnlem2  25811  amgm  27048  wilthlem2  27126  rpvmasum2  27570  noextendseq  27726  noetasuplem2  27793  noetasuplem4  27795  noetainflem2  27797  noetainflem4  27799  axlowdimlem7  28977  axlowdimlem8  28978  axlowdimlem9  28979  axlowdimlem10  28980  axlowdimlem11  28981  axlowdimlem12  28982  unidifsnne  32561  iundisj2f  32609  fressupp  32702  padct  32736  resf1o  32747  iundisj2fi  32804  fprodeq02  32829  gsummptres2  33038  cycpmconjslem2  33157  cyc3conja  33159  elrspunidl  33435  lbsdiflsp0  33653  dimkerim  33654  locfinref  33801  esummono  34034  esumpad  34035  gsumesum  34039  ldgenpisyslem1  34143  measvuni  34194  pmeasmono  34305  eulerpartlemt  34352  tgoldbachgtde  34653  satfv1lem  35346  fullfunfnv  35927  fullfunfv  35928  opnbnd  36307  pibt2  37399  poimirlem6  37612  poimirlem7  37613  poimirlem15  37621  poimirlem22  37628  ismblfin  37647  evlselv  42573  fsuppssind  42579  diophrw  42746  diophren  42800  tfsconcatfn  43327  tfsconcatfv1  43328  tfsconcatfv2  43329  sumnnodd  45585  sge0ss  46367  meassle  46418  meaunle  46419  meadif  46434  meaiininclem  46441  disjdifb  48657  seposep  48721  iscnrm3rlem1  48736