Theorem disjdif 4379

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

Syntax hints:   = wceq 1538   ∖ cdif 3878   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244

This theorem is referenced by:  unvdif  4381  ssdifin0  4389  difdifdir  4395  fresaun  6523  fresaunres2  6524  fvsnun1  6921  fvsnun2  6922  fveqf1o  7037  ralxpmap  8443  undifixp  8481  difsnen  8582  undom  8588  enfixsn  8609  sucdom2  8610  sbthlem7  8617  sbthlem8  8618  domunsn  8651  fodomr  8652  domss2  8660  mapdom2  8672  limensuci  8677  phplem2  8681  pssnn  8720  dif1en  8735  unfi  8769  marypha1lem  8881  brwdom2  9021  infdifsn  9104  dif1card  9421  ackbij1lem12  9642  ackbij1lem18  9648  ssfin4  9721  canthp1lem1  10063  grothprim  10245  hashgval  13689  hashinf  13691  hashfxnn0  13693  hashun2  13740  hashun3  13741  hashssdif  13769  hashfun  13794  hashbclem  13806  hashf1lem2  13810  fsumless  15143  cvgcmpce  15165  incexclem  15183  incexc  15184  fprodsplit1f  15336  setsfun  16510  setsfun0  16511  setsid  16530  mreexexlem3d  16909  mreexexlem4d  16910  sylow2a  18736  gsumval3a  19016  dprd2da  19157  dpjcntz  19167  dpjdisj  19168  dpjlsm  19169  dpjidcl  19173  ablfac1eu  19188  pwssplit1  19824  frlmsslss2  20464  frlmssuvc1  20483  frlmsslsp  20485  islindf4  20527  mdetdiaglem  21203  mdetrlin  21207  mdetrsca  21208  mdetralt  21213  smadiadet  21275  neitr  21785  nrmsep  21962  regsep2  21981  dfconn2  22024  fbncp  22444  filufint  22525  supnfcls  22625  flimfnfcls  22633  restmetu  23177  xrge0gsumle  23438  volinun  24150  iundisj2  24153  volsup  24160  itg2cnlem2  24366  tdeglem4  24661  amgm  25576  wilthlem2  25654  rpvmasum2  26096  axlowdimlem7  26742  axlowdimlem8  26743  axlowdimlem9  26744  axlowdimlem10  26745  axlowdimlem11  26746  axlowdimlem12  26747  disjdifr  30283  difeq  30289  unidifsnne  30308  disjdifprg  30338  iundisj2f  30353  fressupp  30448  padct  30481  resf1o  30492  iundisj2fi  30546  fprodeq02  30565  gsummptres2  30738  tocycfvres1  30802  tocycfvres2  30803  cycpmfvlem  30804  cycpmfv3  30807  cycpmcl  30808  cycpmconjslem2  30847  cyc3conja  30849  elrspunidl  31014  lbsdiflsp0  31110  dimkerim  31111  locfinref  31194  esummono  31423  esumpad  31424  gsumesum  31428  ldgenpisyslem1  31532  measvuni  31583  measunl  31585  pmeasmono  31692  eulerpartlemt  31739  tgoldbachgtde  32041  satfv1lem  32722  mthmpps  32942  noextendseq  33287  noetalem2  33331  noetalem3  33332  fullfunfnv  33520  fullfunfv  33521  opnbnd  33786  cldbnd  33787  pibt2  34834  poimirlem6  35063  poimirlem7  35064  poimirlem15  35072  poimirlem16  35073  poimirlem19  35076  poimirlem22  35079  poimirlem27  35084  ismblfin  35098  fsuppssind  39459  diophrw  39700  eldioph2lem1  39701  eldioph2lem2  39702  diophren  39754  kelac1  40007  sumnnodd  42272  sge0ss  43051  meassle  43102  meaunle  43103  meadif  43118  meaiininclem  43125  isomenndlem  43169