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

Theorem disjdif 3529
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 3392 . 2  |-  ( A  i^i  B )  C_  A
2 inssdif0 3524 . 2  |-  ( ( A  i^i  B ) 
C_  A  <->  ( A  i^i  ( B  \  A
) )  =  (/) )
31, 2mpbi 201 1  |-  ( A  i^i  ( B  \  A ) )  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1625    \ cdif 3152    i^i cin 3154    C_ wss 3155   (/)c0 3458
This theorem is referenced by:  undifv  3531  ssdifin0  3538  difdifdir  3544  fresaun  5379  fresaunres2  5380  fvsnun1  5678  fvsnun2  5679  fveqf1o  5769  undifixp  6849  difsnen  6941  undom  6947  sbthlem7  6974  sbthlem8  6975  domunsn  7008  fodomr  7009  domss2  7017  mapdom2  7029  limensuci  7034  phplem2  7038  sucdom2  7054  pssnn  7078  dif1enOLD  7087  dif1en  7088  unfi  7121  marypha1lem  7183  brwdom2  7284  infdifsn  7354  cantnf0  7373  dif1card  7635  ackbij1lem12  7854  ackbij1lem18  7860  ssfin4  7933  canthp1lem1  8271  grothprim  8453  hashgval  11336  hashinf  11338  hashf  11340  hashun2  11361  hashun3  11362  hashssdif  11370  hashfun  11385  hashbclem  11386  hashf1lem2  11390  fsumless  12250  cvgcmpce  12272  incexclem  12291  incexc  12292  setsid  13183  mreexexlem3d  13544  mreexexlem4d  13545  sylow2a  14926  gsumval3a  15185  dprd2da  15273  dpjcntz  15283  dpjdisj  15284  dpjlsm  15285  dpjidcl  15289  ablfac1eu  15304  nrmsep  17081  regsep2  17100  dfcon2  17141  fbncp  17530  filufint  17611  supnfcls  17711  flimfnfcls  17719  xrge0gsumle  18334  volinun  18899  iundisj2  18902  volsup  18909  itg2cnlem2  19113  tdeglem4  19442  amgm  20281  wilthlem2  20303  rpvmasum2  20657  fullfunfnv  23893  fullfunfv  23894  axlowdimlem7  23985  axlowdimlem8  23986  axlowdimlem9  23987  axlowdimlem10  23988  axlowdimlem11  23989  axlowdimlem12  23990  opnbnd  25644  cldbnd  25645  ralxpmap  26162  diophrw  26239  eldioph2lem1  26240  eldioph2lem2  26241  diophren  26297  kelac1  26562  pwssplit1  26589  frlmsslss2  26646  frlmssuvc1  26647  frlmsslsp  26649  enfixsn  26658  islindf4  26709
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-v 2793  df-dif 3158  df-in 3162  df-ss 3169  df-nul 3459
  Copyright terms: Public domain W3C validator