Theorem disjdif 3900

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

Proof of Theorem disjdif

Step	Hyp	Ref	Expression
1		inss1 3717	. 2
2		inssdif0 3895	. 2
3	1, 2	mpbi 208	1

Syntax hints:  =wceq 1395  \cdif 3472  i^icin 3474  C_wss 3475  c0 3784

This theorem is referenced by:  unvdif  3902  ssdifin0  3909  difdifdir  3915  fresaun  5761  fresaunres2  5762  fvsnun1  6106  fvsnun2  6107  fveqf1o  6205  ralxpmap  7488  undifixp  7525  difsnen  7619  undom  7625  enfixsn  7646  sbthlem7  7653  sbthlem8  7654  domunsn  7687  fodomr  7688  domss2  7696  mapdom2  7708  limensuci  7713  phplem2  7717  sucdom2  7734  pssnn  7758  dif1enOLD  7772  dif1en  7773  unfi  7807  marypha1lem  7913  brwdom2  8020  infdifsn  8094  dif1card  8409  ackbij1lem12  8632  ackbij1lem18  8638  ssfin4  8711  canthp1lem1  9051  grothprim  9233  hashgval  12408  hashinf  12410  hashf  12412  hashun2  12451  hashun3  12452  hashssdif  12475  hashfun  12495  hashbclem  12501  hashf1lem2  12505  fsumless  13610  cvgcmpce  13632  incexclem  13648  incexc  13649  setsid  14673  mreexexlem3d  15043  mreexexlem4d  15044  sylow2a  16639  gsumval3a  16905  gsumval3aOLD  16906  dprd2da  17091  dpjcntz  17101  dpjdisj  17102  dpjlsm  17103  dpjidcl  17107  dpjidclOLD  17114  ablfac1eu  17124  pwssplit1  17705  frlmsslss2  18805  frlmsslss2OLD  18806  frlmssuvc1  18825  frlmssuvc1OLD  18827  frlmsslsp  18829  frlmsslspOLD  18830  islindf4  18873  mdetdiaglem  19100  mdetrlin  19104  mdetrsca  19105  mdetralt  19110  smadiadet  19172  neitr  19681  nrmsep  19858  regsep2  19877  dfcon2  19920  fbncp  20340  filufint  20421  supnfcls  20521  flimfnfcls  20529  restmetu  21090  xrge0gsumle  21338  volinun  21956  iundisj2  21959  volsup  21966  itg2cnlem2  22169  tdeglem4  22458  amgm  23320  wilthlem2  23343  rpvmasum2  23697  axlowdimlem7  24251  axlowdimlem8  24252  axlowdimlem9  24253  axlowdimlem10  24254  axlowdimlem11  24255  axlowdimlem12  24256  difeq  27416  disjdifprg  27436  iundisj2f  27449  resf1o  27553  iundisj2fi  27602  locfinref  27844  esummono  28066  gsumesum  28067  measvuni  28185  measunl  28187  eulerpartlemt  28310  mthmpps  28942  fullfunfnv  29596  fullfunfv  29597  ismblfin  30055  opnbnd  30143  cldbnd  30144  diophrw  30692  eldioph2lem1  30693  eldioph2lem2  30694  diophren  30747  kelac1  31009  fprodsplit1f  31593  sumnnodd  31636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785