Theorem disjdif 4436

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		ssid 3962	. 2 ⊢ 𝐴 ⊆ 𝐴
2		disjdifg 4435	. 2 ⊢ (𝐴 ⊆ 𝐴 → (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅)
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3905   ∩ cin 3907   ⊆ wss 3908  ∅c0 4289

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-in 3915  df-ss 3925  df-nul 4290

This theorem is used by:  disjdifr  4437  unvdif  4439  difdifdir  4457  fresaun  6756  fresaunres2  6757  fvsnun2  7188  undifixp  8941  undom  9063  enfixsn  9084  sbthlem7  9091  sbthlem8  9092  fodomr  9126  domss2  9134  mapdom2  9146  sucdom2  9197  dif1ennnALT  9247  fodomfir  9297  marypha1lem  9403  brwdom2  9545  infdifsn  9636  ackbij1lem12  10232  ssfin4  10312  hashinf  14391  hashfxnn0  14393  hashun2  14439  hashun3  14440  hashssdif  14469  hashfun  14494  hashf1lem2  14513  fsumless  15874  cvgcmpce  15896  incexclem  15916  incexc  15917  fprodsplit1f  16070  mreexexlem3d  17727  sylow2a  19720  gsumval3a  20004  dprd2da  20145  dpjcntz  20155  dpjdisj  20156  dpjlsm  20157  dpjidcl  20161  ablfac1eu  20176  pwssplit1  21217  frlmsslss2  21962  frlmssuvc1  21981  psdmul  22366  mdetdiaglem  22792  mdetrlin  22796  mdetrsca  22797  mdetralt  22802  smadiadet  22864  nrmsep  23551  dfconn2  23613  fbncp  24033  filufint  24114  supnfcls  24214  flimfnfcls  24222  xrge0gsumle  25028  iundisj2  25745  volsup  25752  itg2cnlem2  25958  amgm  27192  wilthlem2  27270  rpvmasum2  27713  noextendseq  27868  noetasuplem2  27935  noetasuplem4  27937  noetainflem2  27939  noetainflem4  27941  axlowdimlem7  29335  axlowdimlem8  29336  axlowdimlem9  29337  axlowdimlem10  29338  axlowdimlem11  29339  axlowdimlem12  29340  unidifsnne  32919  iundisj2f  32972  fressupp  33070  padct  33100  resf1o  33112  iundisj2fi  33179  fprodeq02  33205  gsummptres2  33404  cycpmconjslem2  33506  cyc3conja  33508  gsumind  33696  elrspunidl  33767  lbsdiflsp0  34047  dimkerim  34048  locfinref  34262  esummono  34475  esumpad  34476  gsumesum  34480  ldgenpisyslem1  34584  measvuni  34635  pmeasmono  34745  eulerpartlemt  34792  tgoldbachgtde  35078  satfv1lem  35874  fullfunfnv  36458  fullfunfv  36459  opnbnd  36876  pibt2  38103  poimirlem6  38317  poimirlem7  38318  poimirlem15  38326  poimirlem22  38333  ismblfin  38352  evlselv  43361  fsuppssind  43365  diophrw  43530  diophren  43580  tfsconcatfn  44105  tfsconcatfv1  44106  tfsconcatfv2  44107  sumnnodd  46386  sge0ss  47166  meassle  47217  meaunle  47218  meadif  47233  meaiininclem  47240  disjdifb  49628  seposep  49744  iscnrm3rlem1  49758