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

Theorem disjdif 3700
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 3561 . 2  |-  ( A  i^i  B )  C_  A
2 inssdif0 3695 . 2  |-  ( ( A  i^i  B ) 
C_  A  <->  ( A  i^i  ( B  \  A
) )  =  (/) )
31, 2mpbi 200 1  |-  ( A  i^i  ( B  \  A ) )  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1652    \ cdif 3317    i^i cin 3319    C_ wss 3320   (/)c0 3628
This theorem is referenced by:  undifv  3702  ssdifin0  3709  difdifdir  3715  fresaun  5614  fresaunres2  5615  fvsnun1  5928  fvsnun2  5929  fveqf1o  6029  undifixp  7098  difsnen  7190  undom  7196  sbthlem7  7223  sbthlem8  7224  domunsn  7257  fodomr  7258  domss2  7266  mapdom2  7278  limensuci  7283  phplem2  7287  sucdom2  7303  pssnn  7327  dif1enOLD  7340  dif1en  7341  unfi  7374  marypha1lem  7438  brwdom2  7541  infdifsn  7611  cantnf0  7630  dif1card  7892  ackbij1lem12  8111  ackbij1lem18  8117  ssfin4  8190  canthp1lem1  8527  grothprim  8709  hashgval  11621  hashinf  11623  hashf  11625  hashun2  11657  hashun3  11658  hashssdif  11677  hashfun  11700  hashbclem  11701  hashf1lem2  11705  fsumless  12575  cvgcmpce  12597  incexclem  12616  incexc  12617  setsid  13508  mreexexlem3d  13871  mreexexlem4d  13872  sylow2a  15253  gsumval3a  15512  dprd2da  15600  dpjcntz  15610  dpjdisj  15611  dpjlsm  15612  dpjidcl  15616  ablfac1eu  15631  neitr  17244  nrmsep  17421  regsep2  17440  dfcon2  17482  fbncp  17871  filufint  17952  supnfcls  18052  flimfnfcls  18060  restmetu  18617  xrge0gsumle  18864  volinun  19440  iundisj2  19443  volsup  19450  itg2cnlem2  19654  tdeglem4  19983  amgm  20829  wilthlem2  20852  rpvmasum2  21206  difeq  23998  disjdifprg  24017  iundisj2f  24030  iundisj2fi  24153  esummono  24450  gsumesum  24451  measvuni  24568  measunl  24570  fullfunfnv  25791  fullfunfv  25792  axlowdimlem7  25887  axlowdimlem8  25888  axlowdimlem9  25889  axlowdimlem10  25890  axlowdimlem11  25891  axlowdimlem12  25892  ismblfin  26247  opnbnd  26328  cldbnd  26329  ralxpmap  26742  diophrw  26817  eldioph2lem1  26818  eldioph2lem2  26819  diophren  26874  kelac1  27138  pwssplit1  27165  frlmsslss2  27222  frlmssuvc1  27223  frlmsslsp  27225  enfixsn  27234  islindf4  27285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-v 2958  df-dif 3323  df-in 3327  df-ss 3334  df-nul 3629
  Copyright terms: Public domain W3C validator