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

Theorem ss0 3618
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 3617 . 2  |-  ( A 
C_  (/)  <->  A  =  (/) )
21biimpi 187 1  |-  ( A 
C_  (/)  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3280   (/)c0 3588
This theorem is referenced by:  sseq0  3619  abf  3621  eq0rdv  3622  ssdisj  3637  disjpss  3638  0dif  3659  dfopif  3941  fr0  4521  tfindsg  4799  findsg  4831  poirr2  5217  sofld  5277  f00  5587  frxp  6415  map0b  7011  sbthlem7  7182  phplem2  7246  fi0  7383  cantnflem1  7601  rankeq0b  7742  grur1a  8650  ixxdisj  10887  icodisj  10978  ioodisj  10982  uzdisj  11074  hashf1lem2  11660  sumz  12471  sumss  12473  fsum2dlem  12509  symgbas  15050  cntzval  15075  oppglsm  15231  efgval  15304  islss  15966  00lss  15973  mplsubglem  16453  ntrcls0  17095  neindisj2  17142  hauscmplem  17423  fbdmn0  17819  fbncp  17824  opnfbas  17827  fbasfip  17853  fbunfip  17854  fgcl  17863  supfil  17880  ufinffr  17914  alexsubALTlem2  18032  metnrmlem3  18844  itg1addlem4  19544  mdeg0  19946  uc1pval  20015  mon1pval  20017  pserulm  20291  vdgrun  21625  vdgrfiun  21626  imadifxp  23991  measunl  24523  truae  24547  derangsn  24809  prod1  25223  prodss  25226  fprodss  25227  fprod2dlem  25257  ismblfin  26146  coeq0i  26701  eldioph2lem2  26709  eldioph4b  26762  pcl0N  30404  pcl0bN  30405
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283  df-in 3287  df-ss 3294  df-nul 3589
  Copyright terms: Public domain W3C validator