Theorem ss0 4367

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3916  ∅c0 4298

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-dif 3919  df-ss 3933  df-nul 4299

This theorem is referenced by:  sseq0  4368  0dif  4370  eq0rdvALT  4373  ssdisj  4425  disjpss  4426  dfopif  4836  iunxdif3  5061  fr0  5618  poirr2  6099  sofld  6162  f00  6744  fvmptopab  7445  tfindsg  7839  findsg  7875  frxp  8107  map0b  8858  sbthlem7  9062  ssfi  9142  fi0  9377  cantnflem1  9648  rankeq0b  9819  grur1a  10778  ixxdisj  13327  icodisj  13443  ioodisj  13449  uzdisj  13564  nn0disj  13611  hashf1lem2  14427  swrd0  14629  xptrrel  14952  sumz  15694  sumss  15696  fsum2dlem  15742  prod1  15916  prodss  15919  fprodss  15920  fprod2dlem  15952  cntzval  19259  oppglsm  19578  efgval  19653  islss  20846  00lss  20853  mplsubglem  21914  ntrcls0  22969  neindisj2  23016  hauscmplem  23299  fbdmn0  23727  fbncp  23732  opnfbas  23735  fbasfip  23761  fbunfip  23762  fgcl  23771  supfil  23788  ufinffr  23822  alexsubALTlem2  23941  metnrmlem3  24756  itg1addlem4  25606  uc1pval  26051  mon1pval  26053  pserulm  26337  vtxdun  29415  vtxdginducedm1  29477  difres  32535  imadifxp  32536  swrdrndisj  32885  cycpmco2f1  33087  erlval  33215  ssdifidllem  33433  ply1dg3rt0irred  33557  esumrnmpt2  34064  truae  34239  carsgclctunlem2  34316  acycgr0v  35135  prclisacycgr  35138  derangsn  35157  poimirlem3  37612  ismblfin  37650  pcl0N  39911  pcl0bN  39912  coeq0i  42734  eldioph2lem2  42742  eldioph4b  42792  oe0suclim  43259  ntrk2imkb  44019  ntrk0kbimka  44021  ssin0  45042  iccdifprioo  45507  sumnnodd  45621  sge0split  46400  iscnrm3llem2  48928  0setrec  49683