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

Theorem ss0 3815
Description: Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.)
Assertion
Ref Expression
ss0  |-  ( A 
C_  (/)  ->  A  =  (/) )

Proof of Theorem ss0
StepHypRef Expression
1 ss0b 3814 . 2  |-  ( A 
C_  (/)  <->  A  =  (/) )
21biimpi 194 1  |-  ( A 
C_  (/)  ->  A  =  (/) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    C_ wss 3461   (/)c0 3783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-dif 3464  df-in 3468  df-ss 3475  df-nul 3784
This theorem is referenced by:  sseq0  3816  abf  3818  eq0rdv  3819  ssdisj  3864  disjpss  3865  0dif  3887  dfopif  4200  fr0  4847  poirr2  5379  sofld  5439  f00  5749  tfindsg  6668  findsg  6700  frxp  6883  map0b  7450  sbthlem7  7626  phplem2  7690  fi0  7872  cantnflem1  8099  cantnflem1OLD  8122  rankeq0b  8269  grur1a  9186  ixxdisj  11547  icodisj  11648  ioodisj  11653  uzdisj  11755  nn0disj  11795  hashf1lem2  12492  swrd0  12653  xptrrel  12901  sumz  13629  sumss  13631  fsum2dlem  13670  prod1  13836  prodss  13839  fprodss  13840  fprod2dlem  13869  cntzval  16561  symgbas  16607  oppglsm  16864  efgval  16937  islss  17779  00lss  17786  mplsubglem  18291  mplsubglemOLD  18293  ntrcls0  19747  neindisj2  19794  hauscmplem  20076  fbdmn0  20504  fbncp  20509  opnfbas  20512  fbasfip  20538  fbunfip  20539  fgcl  20548  supfil  20565  ufinffr  20599  alexsubALTlem2  20717  metnrmlem3  21534  itg1addlem4  22275  uc1pval  22709  mon1pval  22711  pserulm  22986  vdgrun  25106  vdgrfiun  25107  iunxdif3  27640  difres  27674  imadifxp  27675  esumrnmpt2  28300  truae  28455  carsgclctunlem2  28530  derangsn  28881  ismblfin  30298  coeq0i  30928  eldioph2lem2  30936  eldioph4b  30987  iccdifprioo  31798  sumnnodd  31878  pcl0N  36062  pcl0bN  36063
  Copyright terms: Public domain W3C validator