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

Theorem disjdif 3468
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 3331 . 2  |-  ( A  i^i  B )  C_  A
2 inssdif0 3463 . 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 3091    i^i cin 3093    C_ wss 3094   (/)c0 3397
This theorem is referenced by:  undifv  3470  ssdifin0  3477  difdifdir  3483  fresaun  5315  fresaunres2  5316  fvsnun1  5614  fvsnun2  5615  fveqf1o  5705  undifixp  6785  difsnen  6877  undom  6883  sbthlem7  6910  sbthlem8  6911  domunsn  6944  fodomr  6945  domss2  6953  mapdom2  6965  limensuci  6970  phplem2  6974  sucdom2  6990  pssnn  7014  dif1enOLD  7023  dif1en  7024  unfi  7057  marypha1lem  7119  brwdom2  7220  infdifsn  7290  cantnf0  7309  dif1card  7571  ackbij1lem12  7790  ackbij1lem18  7796  ssfin4  7869  canthp1lem1  8207  grothprim  8389  hashgval  11271  hashinf  11273  hashf  11275  hashun2  11296  hashssdif  11304  hashfun  11319  hashbclem  11320  hashf1lem2  11324  fsumless  12184  cvgcmpce  12206  setsid  13114  mreexexlem3d  13475  mreexexlem4d  13476  sylow2a  14857  gsumval3a  15116  dprd2da  15204  dpjcntz  15214  dpjdisj  15215  dpjlsm  15216  dpjidcl  15220  ablfac1eu  15235  nrmsep  17012  regsep2  17031  dfcon2  17072  fbncp  17461  filufint  17542  supnfcls  17642  flimfnfcls  17650  xrge0gsumle  18265  volinun  18830  iundisj2  18833  volsup  18840  itg2cnlem2  19044  tdeglem4  19373  amgm  20212  wilthlem2  20234  rpvmasum2  20588  fullfunfnv  23824  fullfunfv  23825  axlowdimlem7  23916  axlowdimlem8  23917  axlowdimlem9  23918  axlowdimlem10  23919  axlowdimlem11  23920  axlowdimlem12  23921  opnbnd  25575  cldbnd  25576  ralxpmap  26093  diophrw  26170  eldioph2lem1  26171  eldioph2lem2  26172  diophren  26228  kelac1  26493  pwssplit1  26520  frlmsslss2  26577  frlmssuvc1  26578  frlmsslsp  26580  enfixsn  26589  islindf4  26640
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-v 2742  df-dif 3097  df-in 3101  df-ss 3108  df-nul 3398
  Copyright terms: Public domain W3C validator