Theorem ss0 4360

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-dif 3909  df-ss 3923  df-nul 4288

This theorem is referenced by:  0dif  4364  eq0rdvALT  4374  ssdisj  4421  disjpss  4422  dfopif  4836  iunxdif3  5062  fr0  5641  poirr2  6126  sofld  6187  f00  6762  fvmptopab  7467  tfindsg  7858  findsg  7895  frxp  8123  map0b  8882  sbthlem7  9082  ssfi  9158  fi0  9381  cantnflem1  9659  rankeq0b  9833  grur1a  10805  ixxdisj  13388  icodisj  13504  ioodisj  13510  uzdisj  13627  nn0disj  13674  hashf1lem2  14495  swrd0  14698  xptrrel  15019  sumz  15775  sumss  15777  fsum2dlem  15823  prod1  16000  prodss  16003  fprodss  16004  fprod2dlem  16036  cntzval  19392  oppglsm  19713  efgval  19788  islss  21036  00lss  21043  ssdifidllem  21465  mplsubglem  22129  ntrcls0  23214  neindisj2  23261  hauscmplem  23544  fbdmn0  23972  fbncp  23977  opnfbas  23980  fbasfip  24006  fbunfip  24007  fgcl  24016  supfil  24033  ufinffr  24067  alexsubALTlem2  24186  metnrmlem3  25000  itg1addlem4  25839  uc1pval  26278  mon1pval  26280  pserulm  26563  vtxdun  29809  vtxdginducedm1  29871  difres  32923  imadifxp  32924  swrdrndisj  33255  cycpmco2f1  33422  erlval  33556  ply1dg3rt0irred  33852  esumrnmpt2  34436  truae  34611  carsgclctunlem2  34687  scott0i  35497  acycgr0v  35618  prclisacycgr  35621  derangsn  35640  ttc00  36997  poimirlem3  38252  ismblfin  38290  pcl0N  40674  pcl0bN  40675  coeq0i  43464  eldioph2lem2  43472  eldioph4b  43518  oe0suclim  43984  ntrk2imkb  44743  ntrk0kbimka  44745  ssin0  45755  iccdifprioo  46212  sumnnodd  46326  sge0split  47103  iscnrm3llem2  49705  0setrec  50459