MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  disjdif Structured version   Visualization version   GIF version

Theorem disjdif 3992
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
StepHypRef Expression
1 inss1 3795 . 2 (𝐴𝐵) ⊆ 𝐴
2 inssdif0 3901 . 2 ((𝐴𝐵) ⊆ 𝐴 ↔ (𝐴 ∩ (𝐵𝐴)) = ∅)
31, 2mpbi 219 1 (𝐴 ∩ (𝐵𝐴)) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  cdif 3537  cin 3539  wss 3540  c0 3874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875
This theorem is referenced by:  unvdif  3994  ssdifin0  4002  difdifdir  4008  fresaun  5988  fresaunres2  5989  fvsnun1  6353  fvsnun2  6354  fveqf1o  6457  ralxpmap  7793  undifixp  7830  difsnen  7927  undom  7933  enfixsn  7954  sbthlem7  7961  sbthlem8  7962  domunsn  7995  fodomr  7996  domss2  8004  mapdom2  8016  limensuci  8021  phplem2  8025  sucdom2  8041  pssnn  8063  dif1en  8078  unfi  8112  marypha1lem  8222  brwdom2  8361  infdifsn  8437  dif1card  8716  ackbij1lem12  8936  ackbij1lem18  8942  ssfin4  9015  canthp1lem1  9353  grothprim  9535  hashgval  12982  hashinf  12984  hashfxnn0  12986  hashfOLD  12988  hashun2  13033  hashun3  13034  hashssdif  13061  hashfun  13084  hashbclem  13093  hashf1lem2  13097  fsumless  14369  cvgcmpce  14391  incexclem  14407  incexc  14408  fprodsplit1f  14560  setsfun  15725  setsfun0  15726  setsid  15742  mreexexlem3d  16129  mreexexlem4d  16130  sylow2a  17857  gsumval3a  18127  dprd2da  18264  dpjcntz  18274  dpjdisj  18275  dpjlsm  18276  dpjidcl  18280  ablfac1eu  18295  pwssplit1  18880  frlmsslss2  19933  frlmssuvc1  19952  frlmsslsp  19954  islindf4  19996  mdetdiaglem  20223  mdetrlin  20227  mdetrsca  20228  mdetralt  20233  smadiadet  20295  neitr  20794  nrmsep  20971  regsep2  20990  dfcon2  21032  fbncp  21453  filufint  21534  supnfcls  21634  flimfnfcls  21642  restmetu  22185  xrge0gsumle  22444  volinun  23121  iundisj2  23124  volsup  23131  itg2cnlem2  23335  tdeglem4  23624  amgm  24517  wilthlem2  24595  rpvmasum2  25001  axlowdimlem7  25628  axlowdimlem8  25629  axlowdimlem9  25630  axlowdimlem10  25631  axlowdimlem11  25632  axlowdimlem12  25633  difeq  28739  disjdifprg  28770  iundisj2f  28785  padct  28885  resf1o  28893  iundisj2fi  28943  locfinref  29236  esummono  29443  esumpad  29444  gsumesum  29448  ldgenpisyslem1  29553  measvuni  29604  measunl  29606  pmeasmono  29713  eulerpartlemt  29760  mthmpps  30733  fullfunfnv  31223  fullfunfv  31224  opnbnd  31490  cldbnd  31491  poimirlem6  32585  poimirlem7  32586  poimirlem15  32594  poimirlem16  32595  poimirlem19  32598  poimirlem22  32601  poimirlem27  32606  ismblfin  32620  diophrw  36340  eldioph2lem1  36341  eldioph2lem2  36342  diophren  36395  kelac1  36651  sumnnodd  38697  sge0ss  39305  meassle  39356  meaunle  39357  meadif  39372  meaiininclem  39376  isomenndlem  39420
  Copyright terms: Public domain W3C validator