Theorem ss0 4351

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-dif 4047  df-nul 4279

This theorem is used by:  0dif  4355  eq0rdvALT  4365  ssdisj  4412  disjpss  4413  dfopif  4836  iunxdif3  5054  fr0  5628  poirr2  6117  sofld  6178  f00  6764  fvmptopab  7475  tfindsg  7872  findsg  7909  frxp  8140  map0b  8914  sbthlem7  9115  ssfi  9191  fi0  9415  cantnflem1  9693  rankeq0b  9879  scott0  9939  grur1a  10907  ixxdisj  13494  icodisj  13610  ioodisj  13616  uzdisj  13734  nn0disj  13781  hashf1lem2  14604  swrd0  14812  xptrrel  15138  sumz  15893  sumss  15895  fsum2dlem  15941  prod1  16116  prodss  16119  fprodss  16120  fprod2dlem  16152  cntzval  19540  oppglsm  19861  efgval  19936  islss  21214  00lss  21221  ssdifidllem  21645  mplsubglem  22311  ntrcls0  23399  neindisj2  23446  hauscmplem  23729  fbdmn0  24158  fbncp  24163  opnfbas  24166  fbasfip  24192  fbunfip  24193  fgcl  24202  supfil  24219  ufinffr  24253  alexsubALTlem2  24372  metnrmlem3  25186  itg1addlem4  26025  uc1pval  26463  mon1pval  26465  pserulm  26754  vtxdun  30067  vtxdginducedm1  30129  difres  33241  imadifxp  33242  swrdrndisj  33564  cycpmco2f1  33731  erlval  33865  ply1dg3rt0irred  34162  esumrnmpt2  34746  truae  34922  carsgclctunlem2  34997  acycgr0v  35989  prclisacycgr  35992  derangsn  36021  ttc00  37388  poimirlem3  38634  ismblfin  38672  pcl0N  41072  pcl0bN  41073  coeq0i  43857  eldioph2lem2  43865  eldioph4b  43911  oe0suclim  44372  ntrk2imkb  45130  ntrk0kbimka  45132  ssin0  46165  iccdifprioo  46621  sumnnodd  46735  sge0split  47512  iscnrm3llem2  50157  0setrec  50965