Theorem ss0 4352

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936  ∅c0 4291

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-dif 3939  df-in 3943  df-ss 3952  df-nul 4292

This theorem is referenced by:  sseq0  4353  0dif  4355  eq0rdv  4357  ssdisj  4409  disjpss  4410  dfopif  4800  iunxdif3  5017  fr0  5534  poirr2  5984  sofld  6044  f00  6561  tfindsg  7575  findsg  7609  frxp  7820  map0b  8447  sbthlem7  8633  phplem2  8697  fi0  8884  cantnflem1  9152  rankeq0b  9289  grur1a  10241  ixxdisj  12754  icodisj  12863  ioodisj  12869  uzdisj  12981  nn0disj  13024  hashf1lem2  13815  swrd0  14020  xptrrel  14340  sumz  15079  sumss  15081  fsum2dlem  15125  prod1  15298  prodss  15301  fprodss  15302  fprod2dlem  15334  cntzval  18451  oppglsm  18767  efgval  18843  islss  19706  00lss  19713  mplsubglem  20214  ntrcls0  21684  neindisj2  21731  hauscmplem  22014  fbdmn0  22442  fbncp  22447  opnfbas  22450  fbasfip  22476  fbunfip  22477  fgcl  22486  supfil  22503  ufinffr  22537  alexsubALTlem2  22656  metnrmlem3  23469  itg1addlem4  24300  uc1pval  24733  mon1pval  24735  pserulm  25010  vtxdun  27263  vtxdginducedm1  27325  difres  30350  imadifxp  30351  swrdrndisj  30631  cycpmco2f1  30766  esumrnmpt2  31327  truae  31502  carsgclctunlem2  31577  acycgr0v  32395  prclisacycgr  32398  derangsn  32417  poimirlem3  34910  ismblfin  34948  pcl0N  37073  pcl0bN  37074  coeq0i  39370  eldioph2lem2  39378  eldioph4b  39428  ntrk2imkb  40407  ntrk0kbimka  40409  ssin0  41337  iccdifprioo  41812  sumnnodd  41931  sge0split  42711  0setrec  44826