Theorem ss0 4337

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

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3890  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-dif 3893  df-ss 3907  df-nul 4269

This theorem is referenced by:  sseq0  4338  0dif  4340  eq0rdvALT  4343  ssdisj  4395  disjpss  4396  dfopif  4808  iunxdif3  5031  fr0  5603  poirr2  6081  sofld  6145  f00  6716  fvmptopab  7418  tfindsg  7808  findsg  7844  frxp  8073  map0b  8828  sbthlem7  9028  ssfi  9104  fi0  9330  cantnflem1  9608  rankeq0b  9782  grur1a  10740  ixxdisj  13311  icodisj  13427  ioodisj  13433  uzdisj  13549  nn0disj  13596  hashf1lem2  14416  swrd0  14619  xptrrel  14940  sumz  15682  sumss  15684  fsum2dlem  15730  prod1  15907  prodss  15910  fprodss  15911  fprod2dlem  15943  cntzval  19294  oppglsm  19615  efgval  19690  islss  20931  00lss  20938  mplsubglem  21980  ntrcls0  23066  neindisj2  23113  hauscmplem  23396  fbdmn0  23824  fbncp  23829  opnfbas  23832  fbasfip  23858  fbunfip  23859  fgcl  23868  supfil  23885  ufinffr  23919  alexsubALTlem2  24038  metnrmlem3  24852  itg1addlem4  25691  uc1pval  26130  mon1pval  26132  pserulm  26412  vtxdun  29575  vtxdginducedm1  29637  difres  32696  imadifxp  32697  swrdrndisj  33043  cycpmco2f1  33212  erlval  33346  ssdifidllem  33546  ply1dg3rt0irred  33674  esumrnmpt2  34259  truae  34434  carsgclctunlem2  34510  acycgr0v  35383  prclisacycgr  35386  derangsn  35405  ttc00  36743  poimirlem3  37997  ismblfin  38035  pcl0N  40421  pcl0bN  40422  coeq0i  43209  eldioph2lem2  43217  eldioph4b  43263  oe0suclim  43729  ntrk2imkb  44488  ntrk0kbimka  44490  ssin0  45510  iccdifprioo  45968  sumnnodd  46082  sge0split  46859  iscnrm3llem2  49447  0setrec  50201