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

Theorem disjdif 3602
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  |-  ( A  i^i  ( B  \  A ) )  =  (/)

Proof of Theorem disjdif
StepHypRef Expression
1 inss1 3465 . 2  |-  ( A  i^i  B )  C_  A
2 inssdif0 3597 . 2  |-  ( ( A  i^i  B ) 
C_  A  <->  ( A  i^i  ( B  \  A
) )  =  (/) )
31, 2mpbi 199 1  |-  ( A  i^i  ( B  \  A ) )  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1642    \ cdif 3225    i^i cin 3227    C_ wss 3228   (/)c0 3531
This theorem is referenced by:  undifv  3604  ssdifin0  3611  difdifdir  3617  fresaun  5492  fresaunres2  5493  fvsnun1  5796  fvsnun2  5797  fveqf1o  5890  undifixp  6937  difsnen  7029  undom  7035  sbthlem7  7062  sbthlem8  7063  domunsn  7096  fodomr  7097  domss2  7105  mapdom2  7117  limensuci  7122  phplem2  7126  sucdom2  7142  pssnn  7166  dif1enOLD  7177  dif1en  7178  unfi  7211  marypha1lem  7273  brwdom2  7374  infdifsn  7444  cantnf0  7463  dif1card  7725  ackbij1lem12  7944  ackbij1lem18  7950  ssfin4  8023  canthp1lem1  8361  grothprim  8543  hashgval  11430  hashinf  11432  hashf  11434  hashun2  11455  hashun3  11456  hashssdif  11464  hashfun  11479  hashbclem  11480  hashf1lem2  11484  fsumless  12345  cvgcmpce  12367  incexclem  12386  incexc  12387  setsid  13278  mreexexlem3d  13641  mreexexlem4d  13642  sylow2a  15023  gsumval3a  15282  dprd2da  15370  dpjcntz  15380  dpjdisj  15381  dpjlsm  15382  dpjidcl  15386  ablfac1eu  15401  nrmsep  17185  regsep2  17204  dfcon2  17245  fbncp  17630  filufint  17711  supnfcls  17811  flimfnfcls  17819  xrge0gsumle  18435  volinun  19001  iundisj2  19004  volsup  19011  itg2cnlem2  19215  tdeglem4  19544  amgm  20390  wilthlem2  20413  rpvmasum2  20767  difeq  23190  disjdifprg  23213  iundisj2f  23225  iundisj2fi  23354  restmetu  23615  esummono  23716  gsumesum  23717  measvuni  23832  measunl  23834  fullfunfnv  25043  fullfunfv  25044  axlowdimlem7  25135  axlowdimlem8  25136  axlowdimlem9  25137  axlowdimlem10  25138  axlowdimlem11  25139  axlowdimlem12  25140  opnbnd  25567  cldbnd  25568  ralxpmap  26084  diophrw  26161  eldioph2lem1  26162  eldioph2lem2  26163  diophren  26219  kelac1  26484  pwssplit1  26511  frlmsslss2  26568  frlmssuvc1  26569  frlmsslsp  26571  enfixsn  26580  islindf4  26631
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-v 2866  df-dif 3231  df-in 3235  df-ss 3242  df-nul 3532
  Copyright terms: Public domain W3C validator