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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3935  ∅c0 4290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-dif 3938  df-in 3942  df-ss 3951  df-nul 4291

This theorem is referenced by:  sseq0  4352  0dif  4354  eq0rdv  4356  ssdisj  4408  disjpss  4409  dfopif  4799  iunxdif3  5016  fr0  5533  poirr2  5983  sofld  6043  f00  6560  tfindsg  7574  findsg  7608  frxp  7819  map0b  8446  sbthlem7  8632  phplem2  8696  fi0  8883  cantnflem1  9151  rankeq0b  9288  grur1a  10240  ixxdisj  12752  icodisj  12861  ioodisj  12867  uzdisj  12979  nn0disj  13022  hashf1lem2  13813  swrd0  14019  xptrrel  14339  sumz  15078  sumss  15080  fsum2dlem  15124  prod1  15297  prodss  15300  fprodss  15301  fprod2dlem  15333  cntzval  18450  oppglsm  18766  efgval  18842  islss  19705  00lss  19712  mplsubglem  20213  ntrcls0  21683  neindisj2  21730  hauscmplem  22013  fbdmn0  22441  fbncp  22446  opnfbas  22449  fbasfip  22475  fbunfip  22476  fgcl  22485  supfil  22502  ufinffr  22536  alexsubALTlem2  22655  metnrmlem3  23468  itg1addlem4  24299  uc1pval  24732  mon1pval  24734  pserulm  25009  vtxdun  27262  vtxdginducedm1  27324  difres  30349  imadifxp  30350  swrdrndisj  30631  cycpmco2f1  30766  esumrnmpt2  31327  truae  31502  carsgclctunlem2  31577  acycgr0v  32395  prclisacycgr  32398  derangsn  32417  poimirlem3  34894  ismblfin  34932  pcl0N  37057  pcl0bN  37058  coeq0i  39348  eldioph2lem2  39356  eldioph4b  39406  ntrk2imkb  40385  ntrk0kbimka  40387  ssin0  41315  iccdifprioo  41790  sumnnodd  41909  sge0split  42690  0setrec  44805