Theorem disjdif 4423

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

Syntax hints:   = wceq 1537   ∖ cdif 3935   ∩ cin 3937   ⊆ wss 3938  ∅c0 4293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-in 3945  df-ss 3954  df-nul 4294

This theorem is referenced by:  unvdif  4425  ssdifin0  4433  difdifdir  4439  fresaun  6551  fresaunres2  6552  fvsnun1  6946  fvsnun2  6947  fveqf1o  7060  ralxpmap  8462  undifixp  8500  difsnen  8601  undom  8607  enfixsn  8628  sbthlem7  8635  sbthlem8  8636  domunsn  8669  fodomr  8670  domss2  8678  mapdom2  8690  limensuci  8695  phplem2  8699  sucdom2  8716  pssnn  8738  dif1en  8753  unfi  8787  marypha1lem  8899  brwdom2  9039  infdifsn  9122  dif1card  9438  ackbij1lem12  9655  ackbij1lem18  9661  ssfin4  9734  canthp1lem1  10076  grothprim  10258  hashgval  13696  hashinf  13698  hashfxnn0  13700  hashun2  13747  hashun3  13748  hashssdif  13776  hashfun  13801  hashbclem  13813  hashf1lem2  13817  fsumless  15153  cvgcmpce  15175  incexclem  15193  incexc  15194  fprodsplit1f  15346  setsfun  16520  setsfun0  16521  setsid  16540  mreexexlem3d  16919  mreexexlem4d  16920  sylow2a  18746  gsumval3a  19025  dprd2da  19166  dpjcntz  19176  dpjdisj  19177  dpjlsm  19178  dpjidcl  19182  ablfac1eu  19197  pwssplit1  19833  frlmsslss2  20921  frlmssuvc1  20940  frlmsslsp  20942  islindf4  20984  mdetdiaglem  21209  mdetrlin  21213  mdetrsca  21214  mdetralt  21219  smadiadet  21281  neitr  21790  nrmsep  21967  regsep2  21986  dfconn2  22029  fbncp  22449  filufint  22530  supnfcls  22630  flimfnfcls  22638  restmetu  23182  xrge0gsumle  23443  volinun  24149  iundisj2  24152  volsup  24159  itg2cnlem2  24365  tdeglem4  24656  amgm  25570  wilthlem2  25648  rpvmasum2  26090  axlowdimlem7  26736  axlowdimlem8  26737  axlowdimlem9  26738  axlowdimlem10  26739  axlowdimlem11  26740  axlowdimlem12  26741  disjdifr  30277  difeq  30282  unidifsnne  30298  disjdifprg  30327  iundisj2f  30342  padct  30457  resf1o  30468  iundisj2fi  30522  fprodeq02  30541  tocycfvres1  30754  tocycfvres2  30755  cycpmfvlem  30756  cycpmfv3  30759  cycpmcl  30760  cycpmconjslem2  30799  cyc3conja  30801  lbsdiflsp0  31024  dimkerim  31025  locfinref  31107  esummono  31315  esumpad  31316  gsumesum  31320  ldgenpisyslem1  31424  measvuni  31475  measunl  31477  pmeasmono  31584  eulerpartlemt  31631  tgoldbachgtde  31933  satfv1lem  32611  mthmpps  32831  noextendseq  33176  noetalem2  33220  noetalem3  33221  fullfunfnv  33409  fullfunfv  33410  opnbnd  33675  cldbnd  33676  pibt2  34700  poimirlem6  34900  poimirlem7  34901  poimirlem15  34909  poimirlem16  34910  poimirlem19  34913  poimirlem22  34916  poimirlem27  34921  ismblfin  34935  diophrw  39363  eldioph2lem1  39364  eldioph2lem2  39365  diophren  39417  kelac1  39670  sumnnodd  41918  sge0ss  42701  meassle  42752  meaunle  42753  meadif  42768  meaiininclem  42775  isomenndlem  42819