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

Theorem disjdif 3526
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 3389 . 2  |-  ( A  i^i  B )  C_  A
2 inssdif0 3521 . 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 1623    \ cdif 3149    i^i cin 3151    C_ wss 3152   (/)c0 3455
This theorem is referenced by:  undifv  3528  ssdifin0  3535  difdifdir  3541  fresaun  5412  fresaunres2  5413  fvsnun1  5715  fvsnun2  5716  fveqf1o  5806  undifixp  6852  difsnen  6944  undom  6950  sbthlem7  6977  sbthlem8  6978  domunsn  7011  fodomr  7012  domss2  7020  mapdom2  7032  limensuci  7037  phplem2  7041  sucdom2  7057  pssnn  7081  dif1enOLD  7090  dif1en  7091  unfi  7124  marypha1lem  7186  brwdom2  7287  infdifsn  7357  cantnf0  7376  dif1card  7638  ackbij1lem12  7857  ackbij1lem18  7863  ssfin4  7936  canthp1lem1  8274  grothprim  8456  hashgval  11340  hashinf  11342  hashf  11344  hashun2  11365  hashun3  11366  hashssdif  11374  hashfun  11389  hashbclem  11390  hashf1lem2  11394  fsumless  12254  cvgcmpce  12276  incexclem  12295  incexc  12296  setsid  13187  mreexexlem3d  13548  mreexexlem4d  13549  sylow2a  14930  gsumval3a  15189  dprd2da  15277  dpjcntz  15287  dpjdisj  15288  dpjlsm  15289  dpjidcl  15293  ablfac1eu  15308  nrmsep  17085  regsep2  17104  dfcon2  17145  fbncp  17534  filufint  17615  supnfcls  17715  flimfnfcls  17723  xrge0gsumle  18338  volinun  18903  iundisj2  18906  volsup  18913  itg2cnlem2  19117  tdeglem4  19446  amgm  20285  wilthlem2  20307  rpvmasum2  20661  difeq  23128  disjdifprg  23352  iundisj2fi  23364  iundisj2f  23366  measvuni  23542  fullfunfnv  24484  fullfunfv  24485  axlowdimlem7  24576  axlowdimlem8  24577  axlowdimlem9  24578  axlowdimlem10  24579  axlowdimlem11  24580  axlowdimlem12  24581  opnbnd  26243  cldbnd  26244  ralxpmap  26761  diophrw  26838  eldioph2lem1  26839  eldioph2lem2  26840  diophren  26896  kelac1  27161  pwssplit1  27188  frlmsslss2  27245  frlmssuvc1  27246  frlmsslsp  27248  enfixsn  27257  islindf4  27308
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456
  Copyright terms: Public domain W3C validator