Theorem ss0 4343

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	⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)

Proof of Theorem ss0

Step	Hyp	Ref	Expression
1		ss0b 4342	. 2 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
2	1	biimpi 216	1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-dif 3893  df-ss 3907  df-nul 4275

This theorem is referenced by:  sseq0  4344  0dif  4346  eq0rdvALT  4349  ssdisj  4401  disjpss  4402  dfopif  4814  iunxdif3  5038  fr0  5602  poirr2  6081  sofld  6145  f00  6716  fvmptopab  7415  tfindsg  7805  findsg  7841  frxp  8069  map0b  8824  sbthlem7  9024  ssfi  9100  fi0  9326  cantnflem1  9601  rankeq0b  9775  grur1a  10733  ixxdisj  13304  icodisj  13420  ioodisj  13426  uzdisj  13542  nn0disj  13589  hashf1lem2  14409  swrd0  14612  xptrrel  14933  sumz  15675  sumss  15677  fsum2dlem  15723  prod1  15900  prodss  15903  fprodss  15904  fprod2dlem  15936  cntzval  19287  oppglsm  19608  efgval  19683  islss  20920  00lss  20927  mplsubglem  21987  ntrcls0  23051  neindisj2  23098  hauscmplem  23381  fbdmn0  23809  fbncp  23814  opnfbas  23817  fbasfip  23843  fbunfip  23844  fgcl  23853  supfil  23870  ufinffr  23904  alexsubALTlem2  24023  metnrmlem3  24837  itg1addlem4  25676  uc1pval  26115  mon1pval  26117  pserulm  26400  vtxdun  29565  vtxdginducedm1  29627  difres  32685  imadifxp  32686  swrdrndisj  33032  cycpmco2f1  33200  erlval  33334  ssdifidllem  33531  ply1dg3rt0irred  33659  esumrnmpt2  34228  truae  34403  carsgclctunlem2  34479  acycgr0v  35346  prclisacycgr  35349  derangsn  35368  ttc00  36706  poimirlem3  37958  ismblfin  37996  pcl0N  40382  pcl0bN  40383  coeq0i  43199  eldioph2lem2  43207  eldioph4b  43257  oe0suclim  43723  ntrk2imkb  44482  ntrk0kbimka  44484  ssin0  45504  iccdifprioo  45964  sumnnodd  46078  sge0split  46855  iscnrm3llem2  49437  0setrec  50191