Theorem disjdif 4426

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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3896   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-in 3906  df-ss 3916  df-nul 4280

This theorem is used by:  disjdifr  4427  unvdif  4429  difdifdir  4447  fresaun  6745  fresaunres2  6746  fvsnun2  7180  undifixp  8946  undom  9068  enfixsn  9089  sbthlem7  9096  sbthlem8  9097  fodomr  9131  domss2  9139  mapdom2  9151  sucdom2  9202  dif1ennnALT  9252  fodomfir  9303  marypha1lem  9409  brwdom2  9551  infdifsn  9642  ackbij1lem12  10289  ssfin4  10369  hashinf  14459  hashfxnn0  14461  hashun2  14507  hashun3  14508  hashssdif  14537  hashfun  14562  hashf1lem2  14581  fsumless  15943  cvgcmpce  15965  incexclem  15985  incexc  15986  fprodsplit1f  16137  mreexexlem3d  17800  sylow2a  19813  gsumval3a  20097  dprd2da  20238  dpjcntz  20248  dpjdisj  20249  dpjlsm  20250  dpjidcl  20254  ablfac1eu  20269  pwssplit1  21314  frlmsslss2  22061  frlmssuvc1  22080  psdmul  22467  mdetdiaglem  22893  mdetrlin  22897  mdetrsca  22898  mdetralt  22903  smadiadet  22965  nrmsep  23655  dfconn2  23717  fbncp  24138  filufint  24219  supnfcls  24319  flimfnfcls  24327  xrge0gsumle  25133  iundisj2  25850  volsup  25857  itg2cnlem2  26063  amgm  27300  wilthlem2  27378  rpvmasum2  27821  noextendseq  28006  noetasuplem2  28073  noetasuplem4  28075  noetainflem2  28077  noetainflem4  28079  axlowdimlem7  29508  axlowdimlem8  29509  axlowdimlem9  29510  axlowdimlem10  29511  axlowdimlem11  29512  axlowdimlem12  29513  unidifsnne  33114  iundisj2f  33166  fressupp  33263  padct  33292  resf1o  33304  iundisj2fi  33371  fprodeq02  33397  gsummptres2  33596  cycpmconjslem2  33698  cyc3conja  33700  gsumind  33888  elrspunidl  33960  lbsdiflsp0  34240  dimkerim  34241  locfinref  34455  esummono  34668  esumpad  34669  gsumesum  34673  ldgenpisyslem1  34778  measvuni  34829  pmeasmono  34939  eulerpartlemt  34986  tgoldbachgtde  35272  satfv1lem  36096  fullfunfnv  36680  fullfunfv  36681  opnbnd  37083  pibt2  38308  poimirlem6  38512  poimirlem7  38513  poimirlem15  38521  poimirlem22  38528  ismblfin  38547  evlselv  43579  fsuppssind  43583  diophrw  43723  diophren  43773  tfsconcatfn  44298  tfsconcatfv1  44299  tfsconcatfv2  44300  sumnnodd  46586  sge0ss  47366  meassle  47417  meaunle  47418  meadif  47433  meaiininclem  47440  disjdifb  49864  seposep  49978  iscnrm3rlem1  49992