Theorem disjdif 4405

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

Syntax hints:   = wceq 1539   ∖ cdif 3884   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904  df-nul 4257

This theorem is referenced by:  disjdifr  4406  unvdif  4408  difdifdir  4422  fresaun  6645  fresaunres2  6646  fvsnun2  7055  undifixp  8722  undom  8846  undomOLD  8847  enfixsn  8868  sucdom2OLD  8869  sbthlem7  8876  sbthlem8  8877  fodomr  8915  domss2  8923  mapdom2  8935  sucdom2  8989  phplem2OLD  9001  pssnnOLD  9040  dif1enALT  9050  unfiOLD  9081  marypha1lem  9192  brwdom2  9332  infdifsn  9415  ackbij1lem12  9987  ssfin4  10066  hashinf  14049  hashfxnn0  14051  hashun2  14098  hashun3  14099  hashssdif  14127  hashfun  14152  hashf1lem2  14170  fsumless  15508  cvgcmpce  15530  incexclem  15548  incexc  15549  fprodsplit1f  15700  mreexexlem3d  17355  sylow2a  19224  gsumval3a  19504  dprd2da  19645  dpjcntz  19655  dpjdisj  19656  dpjlsm  19657  dpjidcl  19661  ablfac1eu  19676  pwssplit1  20321  frlmsslss2  20982  frlmssuvc1  21001  mdetdiaglem  21747  mdetrlin  21751  mdetrsca  21752  mdetralt  21757  smadiadet  21819  nrmsep  22508  dfconn2  22570  fbncp  22990  filufint  23071  supnfcls  23171  flimfnfcls  23179  xrge0gsumle  23996  iundisj2  24713  volsup  24720  itg2cnlem2  24927  tdeglem4OLD  25225  amgm  26140  wilthlem2  26218  rpvmasum2  26660  axlowdimlem7  27316  axlowdimlem8  27317  axlowdimlem9  27318  axlowdimlem10  27319  axlowdimlem11  27320  axlowdimlem12  27321  unidifsnne  30884  iundisj2f  30929  fressupp  31022  padct  31054  resf1o  31065  iundisj2fi  31118  fprodeq02  31137  gsummptres2  31313  cycpmconjslem2  31422  cyc3conja  31424  elrspunidl  31606  lbsdiflsp0  31707  dimkerim  31708  locfinref  31791  esummono  32022  esumpad  32023  gsumesum  32027  ldgenpisyslem1  32131  measvuni  32182  pmeasmono  32291  eulerpartlemt  32338  tgoldbachgtde  32640  satfv1lem  33324  noextendseq  33870  noetasuplem2  33937  noetasuplem4  33939  noetainflem2  33941  noetainflem4  33943  fullfunfnv  34248  fullfunfv  34249  opnbnd  34514  pibt2  35588  poimirlem6  35783  poimirlem7  35784  poimirlem15  35792  poimirlem22  35799  ismblfin  35818  fsuppssind  40282  diophrw  40581  diophren  40635  sumnnodd  43171  sge0ss  43950  meassle  44001  meaunle  44002  meadif  44017  meaiininclem  44024  disjdifb  46155  seposep  46219  iscnrm3rlem1  46234