Theorem disjdif 4471

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

Syntax hints:   = wceq 1542   ∖ cdif 3945   ∩ cin 3947   ⊆ wss 3948  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3951  df-in 3955  df-ss 3965  df-nul 4323

This theorem is referenced by:  disjdifr  4472  unvdif  4474  difdifdir  4491  fresaun  6760  fresaunres2  6761  fvsnun2  7178  undifixp  8925  undom  9056  undomOLD  9057  enfixsn  9078  sucdom2OLD  9079  sbthlem7  9086  sbthlem8  9087  fodomr  9125  domss2  9133  mapdom2  9145  sucdom2  9203  phplem2OLD  9215  pssnnOLD  9262  dif1ennnALT  9274  unfiOLD  9310  marypha1lem  9425  brwdom2  9565  infdifsn  9649  ackbij1lem12  10223  ssfin4  10302  hashinf  14292  hashfxnn0  14294  hashun2  14340  hashun3  14341  hashssdif  14369  hashfun  14394  hashf1lem2  14414  fsumless  15739  cvgcmpce  15761  incexclem  15779  incexc  15780  fprodsplit1f  15931  mreexexlem3d  17587  sylow2a  19482  gsumval3a  19766  dprd2da  19907  dpjcntz  19917  dpjdisj  19918  dpjlsm  19919  dpjidcl  19923  ablfac1eu  19938  pwssplit1  20663  frlmsslss2  21322  frlmssuvc1  21341  mdetdiaglem  22092  mdetrlin  22096  mdetrsca  22097  mdetralt  22102  smadiadet  22164  nrmsep  22853  dfconn2  22915  fbncp  23335  filufint  23416  supnfcls  23516  flimfnfcls  23524  xrge0gsumle  24341  iundisj2  25058  volsup  25065  itg2cnlem2  25272  tdeglem4OLD  25570  amgm  26485  wilthlem2  26563  rpvmasum2  27005  noextendseq  27160  noetasuplem2  27227  noetasuplem4  27229  noetainflem2  27231  noetainflem4  27233  axlowdimlem7  28196  axlowdimlem8  28197  axlowdimlem9  28198  axlowdimlem10  28199  axlowdimlem11  28200  axlowdimlem12  28201  unidifsnne  31761  iundisj2f  31809  fressupp  31898  padct  31932  resf1o  31943  iundisj2fi  31996  fprodeq02  32017  gsummptres2  32193  cycpmconjslem2  32302  cyc3conja  32304  elrspunidl  32535  lbsdiflsp0  32700  dimkerim  32701  locfinref  32810  esummono  33041  esumpad  33042  gsumesum  33046  ldgenpisyslem1  33150  measvuni  33201  pmeasmono  33312  eulerpartlemt  33359  tgoldbachgtde  33661  satfv1lem  34342  fullfunfnv  34907  fullfunfv  34908  opnbnd  35199  pibt2  36287  poimirlem6  36483  poimirlem7  36484  poimirlem15  36492  poimirlem22  36499  ismblfin  36518  evlselv  41157  fsuppssind  41163  diophrw  41483  diophren  41537  tfsconcatfn  42074  tfsconcatfv1  42075  tfsconcatfv2  42076  sumnnodd  44333  sge0ss  45115  meassle  45166  meaunle  45167  meadif  45182  meaiininclem  45189  disjdifb  47448  seposep  47512  iscnrm3rlem1  47527