Theorem ss0 4332

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3887  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904  df-nul 4257

This theorem is referenced by:  sseq0  4333  0dif  4335  eq0rdvALT  4339  ssdisj  4393  disjpss  4394  dfopifOLD  4801  iunxdif3  5024  fr0  5568  poirr2  6029  sofld  6090  f00  6656  fvmptopab  7329  tfindsg  7707  findsg  7746  frxp  7967  map0b  8671  sbthlem7  8876  ssfi  8956  phplem2OLD  9001  fi0  9179  cantnflem1  9447  rankeq0b  9618  grur1a  10575  ixxdisj  13094  icodisj  13208  ioodisj  13214  uzdisj  13329  nn0disj  13372  hashf1lem2  14170  swrd0  14371  xptrrel  14691  sumz  15434  sumss  15436  fsum2dlem  15482  prod1  15654  prodss  15657  fprodss  15658  fprod2dlem  15690  cntzval  18927  oppglsm  19247  efgval  19323  islss  20196  00lss  20203  mplsubglem  21205  ntrcls0  22227  neindisj2  22274  hauscmplem  22557  fbdmn0  22985  fbncp  22990  opnfbas  22993  fbasfip  23019  fbunfip  23020  fgcl  23029  supfil  23046  ufinffr  23080  alexsubALTlem2  23199  metnrmlem3  24024  itg1addlem4  24863  itg1addlem4OLD  24864  uc1pval  25304  mon1pval  25306  pserulm  25581  vtxdun  27848  vtxdginducedm1  27910  difres  30939  imadifxp  30940  swrdrndisj  31229  cycpmco2f1  31391  esumrnmpt2  32036  truae  32211  carsgclctunlem2  32286  acycgr0v  33110  prclisacycgr  33113  derangsn  33132  poimirlem3  35780  ismblfin  35818  pcl0N  37936  pcl0bN  37937  coeq0i  40575  eldioph2lem2  40583  eldioph4b  40633  ntrk2imkb  41647  ntrk0kbimka  41649  ssin0  42603  iccdifprioo  43054  sumnnodd  43171  sge0split  43947  iscnrm3llem2  46244  0setrec  46409