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

Theorem ss0 3650
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 3649 . 2  |-  ( A 
C_  (/)  <->  A  =  (/) )
21biimpi 187 1  |-  ( A 
C_  (/)  ->  A  =  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3312   (/)c0 3620
This theorem is referenced by:  sseq0  3651  abf  3653  eq0rdv  3654  ssdisj  3669  disjpss  3670  0dif  3691  dfopif  3973  fr0  4553  tfindsg  4832  findsg  4864  poirr2  5250  sofld  5310  f00  5620  frxp  6448  map0b  7044  sbthlem7  7215  phplem2  7279  fi0  7417  cantnflem1  7637  rankeq0b  7778  grur1a  8686  ixxdisj  10923  icodisj  11014  ioodisj  11018  uzdisj  11111  hashf1lem2  11697  sumz  12508  sumss  12510  fsum2dlem  12546  symgbas  15087  cntzval  15112  oppglsm  15268  efgval  15341  islss  16003  00lss  16010  mplsubglem  16490  ntrcls0  17132  neindisj2  17179  hauscmplem  17461  fbdmn0  17858  fbncp  17863  opnfbas  17866  fbasfip  17892  fbunfip  17893  fgcl  17902  supfil  17919  ufinffr  17953  alexsubALTlem2  18071  metnrmlem3  18883  itg1addlem4  19583  mdeg0  19985  uc1pval  20054  mon1pval  20056  pserulm  20330  vdgrun  21664  vdgrfiun  21665  imadifxp  24030  measunl  24562  truae  24586  derangsn  24848  prod1  25262  prodss  25265  fprodss  25266  fprod2dlem  25296  ismblfin  26237  coeq0i  26802  eldioph2lem2  26810  eldioph4b  26863  pcl0N  30656  pcl0bN  30657
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315  df-in 3319  df-ss 3326  df-nul 3621
  Copyright terms: Public domain W3C validator