Theorem disjdif 4435

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

Syntax hints:   = wceq 1540   ∖ cdif 3911   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-in 3921  df-ss 3931  df-nul 4297

This theorem is referenced by:  disjdifr  4436  unvdif  4438  difdifdir  4455  fresaun  6731  fresaunres2  6732  fvsnun2  7157  undifixp  8907  undom  9029  enfixsn  9050  sbthlem7  9057  sbthlem8  9058  fodomr  9092  domss2  9100  mapdom2  9112  sucdom2  9167  dif1ennnALT  9222  fodomfir  9279  marypha1lem  9384  brwdom2  9526  infdifsn  9610  ackbij1lem12  10183  ssfin4  10263  hashinf  14300  hashfxnn0  14302  hashun2  14348  hashun3  14349  hashssdif  14377  hashfun  14402  hashf1lem2  14421  fsumless  15762  cvgcmpce  15784  incexclem  15802  incexc  15803  fprodsplit1f  15956  mreexexlem3d  17607  sylow2a  19549  gsumval3a  19833  dprd2da  19974  dpjcntz  19984  dpjdisj  19985  dpjlsm  19986  dpjidcl  19990  ablfac1eu  20005  pwssplit1  20966  frlmsslss2  21684  frlmssuvc1  21703  psdmul  22053  mdetdiaglem  22485  mdetrlin  22489  mdetrsca  22490  mdetralt  22495  smadiadet  22557  nrmsep  23244  dfconn2  23306  fbncp  23726  filufint  23807  supnfcls  23907  flimfnfcls  23915  xrge0gsumle  24722  iundisj2  25450  volsup  25457  itg2cnlem2  25663  amgm  26901  wilthlem2  26979  rpvmasum2  27423  noextendseq  27579  noetasuplem2  27646  noetasuplem4  27648  noetainflem2  27650  noetainflem4  27652  axlowdimlem7  28875  axlowdimlem8  28876  axlowdimlem9  28877  axlowdimlem10  28878  axlowdimlem11  28879  axlowdimlem12  28880  unidifsnne  32465  iundisj2f  32519  fressupp  32611  padct  32643  resf1o  32653  iundisj2fi  32720  fprodeq02  32748  gsummptres2  32993  cycpmconjslem2  33112  cyc3conja  33114  elrspunidl  33399  lbsdiflsp0  33622  dimkerim  33623  locfinref  33831  esummono  34044  esumpad  34045  gsumesum  34049  ldgenpisyslem1  34153  measvuni  34204  pmeasmono  34315  eulerpartlemt  34362  tgoldbachgtde  34651  satfv1lem  35349  fullfunfnv  35934  fullfunfv  35935  opnbnd  36313  pibt2  37405  poimirlem6  37620  poimirlem7  37621  poimirlem15  37629  poimirlem22  37636  ismblfin  37655  evlselv  42575  fsuppssind  42581  diophrw  42747  diophren  42801  tfsconcatfn  43327  tfsconcatfv1  43328  tfsconcatfv2  43329  sumnnodd  45628  sge0ss  46410  meassle  46461  meaunle  46462  meadif  46477  meaiininclem  46484  disjdifb  48798  seposep  48914  iscnrm3rlem1  48928