Theorem disjdif 4445

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

Syntax hints:   = wceq 1539   ∖ cdif 3921   ∩ cin 3923   ⊆ wss 3924  ∅c0 4306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3459  df-dif 3927  df-in 3931  df-ss 3941  df-nul 4307

This theorem is referenced by:  disjdifr  4446  unvdif  4448  difdifdir  4465  fresaun  6746  fresaunres2  6747  fvsnun2  7172  undifixp  8943  undom  9068  undomOLD  9069  enfixsn  9090  sucdom2OLD  9091  sbthlem7  9098  sbthlem8  9099  fodomr  9137  domss2  9145  mapdom2  9157  sucdom2  9212  phplem2OLD  9224  dif1ennnALT  9278  fodomfir  9335  marypha1lem  9440  brwdom2  9580  infdifsn  9664  ackbij1lem12  10237  ssfin4  10317  hashinf  14343  hashfxnn0  14345  hashun2  14391  hashun3  14392  hashssdif  14420  hashfun  14445  hashf1lem2  14464  fsumless  15801  cvgcmpce  15823  incexclem  15841  incexc  15842  fprodsplit1f  15995  mreexexlem3d  17645  sylow2a  19587  gsumval3a  19871  dprd2da  20012  dpjcntz  20022  dpjdisj  20023  dpjlsm  20024  dpjidcl  20028  ablfac1eu  20043  pwssplit1  21004  frlmsslss2  21722  frlmssuvc1  21741  psdmul  22091  mdetdiaglem  22523  mdetrlin  22527  mdetrsca  22528  mdetralt  22533  smadiadet  22595  nrmsep  23282  dfconn2  23344  fbncp  23764  filufint  23845  supnfcls  23945  flimfnfcls  23953  xrge0gsumle  24760  iundisj2  25489  volsup  25496  itg2cnlem2  25702  amgm  26939  wilthlem2  27017  rpvmasum2  27461  noextendseq  27617  noetasuplem2  27684  noetasuplem4  27686  noetainflem2  27688  noetainflem4  27690  axlowdimlem7  28861  axlowdimlem8  28862  axlowdimlem9  28863  axlowdimlem10  28864  axlowdimlem11  28865  axlowdimlem12  28866  unidifsnne  32451  iundisj2f  32505  fressupp  32599  padct  32633  resf1o  32643  iundisj2fi  32711  fprodeq02  32739  gsummptres2  32984  cycpmconjslem2  33103  cyc3conja  33105  elrspunidl  33380  lbsdiflsp0  33601  dimkerim  33602  locfinref  33801  esummono  34014  esumpad  34015  gsumesum  34019  ldgenpisyslem1  34123  measvuni  34174  pmeasmono  34285  eulerpartlemt  34332  tgoldbachgtde  34621  satfv1lem  35313  fullfunfnv  35893  fullfunfv  35894  opnbnd  36272  pibt2  37364  poimirlem6  37579  poimirlem7  37580  poimirlem15  37588  poimirlem22  37595  ismblfin  37614  evlselv  42542  fsuppssind  42548  diophrw  42714  diophren  42768  tfsconcatfn  43294  tfsconcatfv1  43295  tfsconcatfv2  43296  sumnnodd  45595  sge0ss  46377  meassle  46428  meaunle  46429  meadif  46444  meaiininclem  46451  disjdifb  48682  seposep  48794  iscnrm3rlem1  48808