Theorem disjdif 4425

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

Syntax hints:   = wceq 1559   ∖ cdif 3901   ∩ cin 3903   ⊆ wss 3904  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3907  df-in 3911  df-ss 3921  df-nul 4286

This theorem is referenced by:  disjdifr  4426  unvdif  4428  difdifdir  4444  fresaun  6731  fresaunres2  6732  fvsnun2  7163  undifixp  8912  undom  9033  enfixsn  9054  sbthlem7  9061  sbthlem8  9062  fodomr  9096  domss2  9104  mapdom2  9116  sucdom2  9167  dif1ennnALT  9217  fodomfir  9268  marypha1lem  9376  brwdom2  9518  infdifsn  9609  ackbij1lem12  10183  ssfin4  10264  hashinf  14345  hashfxnn0  14347  hashun2  14393  hashun3  14394  hashssdif  14422  hashfun  14447  hashf1lem2  14466  fsumless  15807  cvgcmpce  15829  incexclem  15849  incexc  15850  fprodsplit1f  16003  mreexexlem3d  17661  sylow2a  19642  gsumval3a  19926  dprd2da  20067  dpjcntz  20077  dpjdisj  20078  dpjlsm  20079  dpjidcl  20083  ablfac1eu  20098  pwssplit1  21106  frlmsslss2  21807  frlmssuvc1  21826  psdmul  22211  mdetdiaglem  22638  mdetrlin  22642  mdetrsca  22643  mdetralt  22648  smadiadet  22710  nrmsep  23397  dfconn2  23459  fbncp  23879  filufint  23960  supnfcls  24060  flimfnfcls  24068  xrge0gsumle  24874  iundisj2  25591  volsup  25598  itg2cnlem2  25804  amgm  27032  wilthlem2  27110  rpvmasum2  27553  noextendseq  27708  noetasuplem2  27775  noetasuplem4  27777  noetainflem2  27779  noetainflem4  27781  axlowdimlem7  29095  axlowdimlem8  29096  axlowdimlem9  29097  axlowdimlem10  29098  axlowdimlem11  29099  axlowdimlem12  29100  unidifsnne  32684  iundisj2f  32739  fressupp  32840  padct  32870  resf1o  32882  iundisj2fi  32949  fprodeq02  32976  gsummptres2  33194  cycpmconjslem2  33296  cyc3conja  33298  gsumind  33492  elrspunidl  33575  lbsdiflsp0  33884  dimkerim  33885  locfinref  34099  esummono  34312  esumpad  34313  gsumesum  34317  ldgenpisyslem1  34421  measvuni  34472  pmeasmono  34582  eulerpartlemt  34629  tgoldbachgtde  34918  satfv1lem  35676  fullfunfnv  36260  fullfunfv  36261  opnbnd  36649  pibt2  37875  poimirlem6  38089  poimirlem7  38090  poimirlem15  38098  poimirlem22  38105  ismblfin  38124  evlselv  43135  fsuppssind  43139  diophrw  43304  diophren  43354  tfsconcatfn  43879  tfsconcatfv1  43880  tfsconcatfv2  43881  sumnnodd  46170  sge0ss  46950  meassle  47001  meaunle  47002  meadif  47017  meaiininclem  47024  disjdifb  49395  seposep  49511  iscnrm3rlem1  49525