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 216	1 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅)

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3898  ∅c0 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-dif 3901  df-ss 3915  df-nul 4283

This theorem is referenced by:  sseq0  4352  0dif  4354  eq0rdvALT  4357  ssdisj  4409  disjpss  4410  dfopif  4821  iunxdif3  5045  fr0  5597  poirr2  6075  sofld  6139  f00  6710  fvmptopab  7407  tfindsg  7797  findsg  7833  frxp  8062  map0b  8813  sbthlem7  9013  ssfi  9089  fi0  9311  cantnflem1  9586  rankeq0b  9760  grur1a  10717  ixxdisj  13262  icodisj  13378  ioodisj  13384  uzdisj  13499  nn0disj  13546  hashf1lem2  14365  swrd0  14568  xptrrel  14889  sumz  15631  sumss  15633  fsum2dlem  15679  prod1  15853  prodss  15856  fprodss  15857  fprod2dlem  15889  cntzval  19235  oppglsm  19556  efgval  19631  islss  20869  00lss  20876  mplsubglem  21937  ntrcls0  22992  neindisj2  23039  hauscmplem  23322  fbdmn0  23750  fbncp  23755  opnfbas  23758  fbasfip  23784  fbunfip  23785  fgcl  23794  supfil  23811  ufinffr  23845  alexsubALTlem2  23964  metnrmlem3  24778  itg1addlem4  25628  uc1pval  26073  mon1pval  26075  pserulm  26359  vtxdun  29462  vtxdginducedm1  29524  difres  32582  imadifxp  32583  swrdrndisj  32945  cycpmco2f1  33100  erlval  33232  ssdifidllem  33428  ply1dg3rt0irred  33553  esumrnmpt2  34102  truae  34277  carsgclctunlem2  34353  acycgr0v  35213  prclisacycgr  35216  derangsn  35235  poimirlem3  37683  ismblfin  37721  pcl0N  40041  pcl0bN  40042  coeq0i  42870  eldioph2lem2  42878  eldioph4b  42928  oe0suclim  43394  ntrk2imkb  44154  ntrk0kbimka  44156  ssin0  45176  iccdifprioo  45640  sumnnodd  45754  sge0split  46531  iscnrm3llem2  49074  0setrec  49829