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

Theorem disjdif 3432
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 3296 . 2  |-  ( A  i^i  B )  C_  A
2 inssdif0 3427 . 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 3075    i^i cin 3077    C_ wss 3078   (/)c0 3362
This theorem is referenced by:  undifv  3434  ssdifin0  3441  difdifdir  3447  fresaun  5269  fresaunres2  5270  fvsnun1  5567  fvsnun2  5568  fveqf1o  5658  undifixp  6738  difsnen  6829  undom  6835  sbthlem7  6862  sbthlem8  6863  domunsn  6896  fodomr  6897  domss2  6905  mapdom2  6917  limensuci  6922  phplem2  6926  sucdom2  6942  pssnn  6966  dif1enOLD  6975  dif1en  6976  unfi  7009  marypha1lem  7070  brwdom2  7171  infdifsn  7241  cantnf0  7260  dif1card  7522  ackbij1lem12  7741  ackbij1lem18  7747  ssfin4  7820  canthp1lem1  8154  grothprim  8336  hashgval  11218  hashinf  11220  hashf  11222  hashun2  11243  hashssdif  11251  hashfun  11266  hashbclem  11267  hashf1lem2  11271  fsumless  12131  cvgcmpce  12153  setsid  13061  sylow2a  14765  gsumval3a  15024  dprd2da  15112  dpjcntz  15122  dpjdisj  15123  dpjlsm  15124  dpjidcl  15128  ablfac1eu  15143  nrmsep  16917  regsep2  16936  dfcon2  16977  fbncp  17366  filufint  17447  supnfcls  17547  flimfnfcls  17555  xrge0gsumle  18170  volinun  18735  iundisj2  18738  volsup  18745  itg2cnlem2  18949  tdeglem4  19278  amgm  20117  wilthlem2  20139  rpvmasum2  20493  fullfunfnv  23658  fullfunfv  23659  axlowdimlem7  23750  axlowdimlem8  23751  axlowdimlem9  23752  axlowdimlem10  23753  axlowdimlem11  23754  axlowdimlem12  23755  opnbnd  25409  cldbnd  25410  ralxpmap  25927  diophrw  26004  eldioph2lem1  26005  eldioph2lem2  26006  diophren  26062  kelac1  26327  pwssplit1  26354  frlmsslss2  26411  frlmssuvc1  26412  frlmsslsp  26414  enfixsn  26423  islindf4  26474
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-v 2729  df-dif 3081  df-in 3085  df-ss 3089  df-nul 3363
  Copyright terms: Public domain W3C validator