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

Theorem disjdif 3987
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 3790 . 2 (𝐴𝐵) ⊆ 𝐴
2 inssdif0 3896 . 2 ((𝐴𝐵) ⊆ 𝐴 ↔ (𝐴 ∩ (𝐵𝐴)) = ∅)
31, 2mpbi 218 1 (𝐴 ∩ (𝐵𝐴)) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  cdif 3532  cin 3534  wss 3535  c0 3869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-dif 3538  df-in 3542  df-ss 3549  df-nul 3870
This theorem is referenced by:  unvdif  3989  ssdifin0  3997  difdifdir  4003  fresaun  5969  fresaunres2  5970  fvsnun1  6327  fvsnun2  6328  fveqf1o  6431  ralxpmap  7766  undifixp  7803  difsnen  7900  undom  7906  enfixsn  7927  sbthlem7  7934  sbthlem8  7935  domunsn  7968  fodomr  7969  domss2  7977  mapdom2  7989  limensuci  7994  phplem2  7998  sucdom2  8014  pssnn  8036  dif1en  8051  unfi  8085  marypha1lem  8195  brwdom2  8334  infdifsn  8410  dif1card  8689  ackbij1lem12  8909  ackbij1lem18  8915  ssfin4  8988  canthp1lem1  9326  grothprim  9508  hashgval  12933  hashinf  12935  hashf  12937  hashun2  12981  hashun3  12982  hashssdif  13009  hashfun  13032  hashbclem  13041  hashf1lem2  13045  fsumless  14311  cvgcmpce  14333  incexclem  14349  incexc  14350  fprodsplit1f  14502  setsfun  15667  setsfun0  15668  setsid  15684  mreexexlem3d  16071  mreexexlem4d  16072  sylow2a  17799  gsumval3a  18069  dprd2da  18206  dpjcntz  18216  dpjdisj  18217  dpjlsm  18218  dpjidcl  18222  ablfac1eu  18237  pwssplit1  18822  frlmsslss2  19871  frlmssuvc1  19890  frlmsslsp  19892  islindf4  19934  mdetdiaglem  20161  mdetrlin  20165  mdetrsca  20166  mdetralt  20171  smadiadet  20233  neitr  20732  nrmsep  20909  regsep2  20928  dfcon2  20970  fbncp  21391  filufint  21472  supnfcls  21572  flimfnfcls  21580  restmetu  22122  xrge0gsumle  22372  volinun  23034  iundisj2  23037  volsup  23044  itg2cnlem2  23248  tdeglem4  23537  amgm  24430  wilthlem2  24508  rpvmasum2  24914  axlowdimlem7  25542  axlowdimlem8  25543  axlowdimlem9  25544  axlowdimlem10  25545  axlowdimlem11  25546  axlowdimlem12  25547  difeq  28541  disjdifprg  28572  iundisj2f  28587  padct  28687  resf1o  28695  iundisj2fi  28745  locfinref  29038  esummono  29245  esumpad  29246  gsumesum  29250  ldgenpisyslem1  29355  measvuni  29406  measunl  29408  pmeasmono  29515  eulerpartlemt  29562  mthmpps  30535  fullfunfnv  31025  fullfunfv  31026  opnbnd  31292  cldbnd  31293  poimirlem6  32384  poimirlem7  32385  poimirlem15  32393  poimirlem16  32394  poimirlem19  32397  poimirlem22  32400  poimirlem27  32405  ismblfin  32419  diophrw  36139  eldioph2lem1  36140  eldioph2lem2  36141  diophren  36194  kelac1  36450  sumnnodd  38497  sge0ss  39105  meassle  39156  meaunle  39157  meadif  39172  meaiininclem  39176  isomenndlem  39220
  Copyright terms: Public domain W3C validator