Theorem ss0 4355

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 4354	. 2 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
2	1	biimpi 219	1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-dif 4050  df-nul 4282

This theorem is used by:  0dif  4359  eq0rdvALT  4369  ssdisj  4416  disjpss  4417  dfopif  4840  iunxdif3  5058  fr0  5633  poirr2  6130  sofld  6191  f00  6786  fvmptopab  7498  tfindsg  7896  findsg  7933  frxp  8165  map0b  8939  sbthlem7  9140  ssfi  9216  fi0  9439  cantnflem1  9717  rankeq0b  9903  scott0  9963  grur1a  10931  ixxdisj  13518  icodisj  13634  ioodisj  13640  uzdisj  13758  nn0disj  13805  hashf1lem2  14628  swrd0  14836  xptrrel  15162  sumz  15917  sumss  15919  fsum2dlem  15965  prod1  16140  prodss  16143  fprodss  16144  fprod2dlem  16176  cntzval  19565  oppglsm  19886  efgval  19961  islss  21239  00lss  21246  ssdifidllem  21670  mplsubglem  22336  ntrcls0  23424  neindisj2  23471  hauscmplem  23754  fbdmn0  24183  fbncp  24188  opnfbas  24191  fbasfip  24217  fbunfip  24218  fgcl  24227  supfil  24244  ufinffr  24278  alexsubALTlem2  24397  metnrmlem3  25211  itg1addlem4  26050  uc1pval  26488  mon1pval  26490  pserulm  26779  vtxdun  30092  vtxdginducedm1  30154  difres  33266  imadifxp  33267  swrdrndisj  33588  cycpmco2f1  33755  erlval  33889  ply1dg3rt0irred  34186  esumrnmpt2  34770  truae  34946  carsgclctunlem2  35021  acycgr0v  36070  prclisacycgr  36073  derangsn  36102  ttc00  37474  poimirlem3  38733  ismblfin  38771  pcl0N  41171  pcl0bN  41172  coeq0i  43957  eldioph2lem2  43965  eldioph4b  44011  oe0suclim  44471  ntrk2imkb  45229  ntrk0kbimka  45231  ssin0  46277  iccdifprioo  46733  sumnnodd  46847  sge0split  47624  iscnrm3llem2  50269  0setrec  51077