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

Theorem disjdif 3501
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 3364 . 2  |-  ( A  i^i  B )  C_  A
2 inssdif0 3496 . 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 1619    \ cdif 3124    i^i cin 3126    C_ wss 3127   (/)c0 3430
This theorem is referenced by:  undifv  3503  ssdifin0  3510  difdifdir  3516  fresaun  5350  fresaunres2  5351  fvsnun1  5649  fvsnun2  5650  fveqf1o  5740  undifixp  6820  difsnen  6912  undom  6918  sbthlem7  6945  sbthlem8  6946  domunsn  6979  fodomr  6980  domss2  6988  mapdom2  7000  limensuci  7005  phplem2  7009  sucdom2  7025  pssnn  7049  dif1enOLD  7058  dif1en  7059  unfi  7092  marypha1lem  7154  brwdom2  7255  infdifsn  7325  cantnf0  7344  dif1card  7606  ackbij1lem12  7825  ackbij1lem18  7831  ssfin4  7904  canthp1lem1  8242  grothprim  8424  hashgval  11306  hashinf  11308  hashf  11310  hashun2  11331  hashssdif  11339  hashfun  11354  hashbclem  11355  hashf1lem2  11359  fsumless  12219  cvgcmpce  12241  setsid  13149  mreexexlem3d  13510  mreexexlem4d  13511  sylow2a  14892  gsumval3a  15151  dprd2da  15239  dpjcntz  15249  dpjdisj  15250  dpjlsm  15251  dpjidcl  15255  ablfac1eu  15270  nrmsep  17047  regsep2  17066  dfcon2  17107  fbncp  17496  filufint  17577  supnfcls  17677  flimfnfcls  17685  xrge0gsumle  18300  volinun  18865  iundisj2  18868  volsup  18875  itg2cnlem2  19079  tdeglem4  19408  amgm  20247  wilthlem2  20269  rpvmasum2  20623  fullfunfnv  23859  fullfunfv  23860  axlowdimlem7  23951  axlowdimlem8  23952  axlowdimlem9  23953  axlowdimlem10  23954  axlowdimlem11  23955  axlowdimlem12  23956  opnbnd  25610  cldbnd  25611  ralxpmap  26128  diophrw  26205  eldioph2lem1  26206  eldioph2lem2  26207  diophren  26263  kelac1  26528  pwssplit1  26555  frlmsslss2  26612  frlmssuvc1  26613  frlmsslsp  26615  enfixsn  26624  islindf4  26675
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-v 2765  df-dif 3130  df-in 3134  df-ss 3141  df-nul 3431
  Copyright terms: Public domain W3C validator