Theorem ss0 4306

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

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244

This theorem is referenced by:  sseq0  4307  0dif  4309  eq0rdv  4312  ssdisj  4367  disjpss  4368  dfopif  4760  iunxdif3  4980  fr0  5498  poirr2  5951  sofld  6011  f00  6535  tfindsg  7555  findsg  7590  frxp  7803  map0b  8430  sbthlem7  8617  phplem2  8681  fi0  8868  cantnflem1  9136  rankeq0b  9273  grur1a  10230  ixxdisj  12741  icodisj  12854  ioodisj  12860  uzdisj  12975  nn0disj  13018  hashf1lem2  13810  swrd0  14011  xptrrel  14331  sumz  15071  sumss  15073  fsum2dlem  15117  prod1  15290  prodss  15293  fprodss  15294  fprod2dlem  15326  cntzval  18443  oppglsm  18759  efgval  18835  islss  19699  00lss  19706  mplsubglem  20672  ntrcls0  21681  neindisj2  21728  hauscmplem  22011  fbdmn0  22439  fbncp  22444  opnfbas  22447  fbasfip  22473  fbunfip  22474  fgcl  22483  supfil  22500  ufinffr  22534  alexsubALTlem2  22653  metnrmlem3  23466  itg1addlem4  24303  uc1pval  24740  mon1pval  24742  pserulm  25017  vtxdun  27271  vtxdginducedm1  27333  difres  30363  imadifxp  30364  swrdrndisj  30657  cycpmco2f1  30816  esumrnmpt2  31437  truae  31612  carsgclctunlem2  31687  acycgr0v  32508  prclisacycgr  32511  derangsn  32530  poimirlem3  35060  ismblfin  35098  pcl0N  37218  pcl0bN  37219  coeq0i  39694  eldioph2lem2  39702  eldioph4b  39752  ntrk2imkb  40740  ntrk0kbimka  40742  ssin0  41689  iccdifprioo  42153  sumnnodd  42272  sge0split  43048  0setrec  45233