Theorem ss0 4168

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

Syntax hints:   → wi 4   = wceq 1653   ⊆ wss 3767  ∅c0 4113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-v 3385  df-dif 3770  df-in 3774  df-ss 3781  df-nul 4114

This theorem is referenced by:  sseq0  4169  0dif  4171  eq0rdv  4173  ssdisj  4220  disjpss  4221  dfopif  4588  iunxdif3  4795  fr0  5289  poirr2  5736  sofld  5796  f00  6300  tfindsg  7292  findsg  7325  frxp  7522  map0b  8133  sbthlem7  8316  phplem2  8380  fi0  8566  cantnflem1  8834  rankeq0b  8971  grur1a  9927  ixxdisj  12435  icodisj  12545  ioodisj  12552  uzdisj  12663  nn0disj  12706  hashf1lem2  13485  swrd0  13683  xptrrel  14058  sumz  14790  sumss  14792  fsum2dlem  14836  prod1  15007  prodss  15010  fprodss  15011  fprod2dlem  15043  cntzval  18062  symgbas  18108  oppglsm  18366  efgval  18439  islss  19249  00lss  19256  mplsubglem  19753  ntrcls0  21205  neindisj2  21252  hauscmplem  21534  fbdmn0  21962  fbncp  21967  opnfbas  21970  fbasfip  21996  fbunfip  21997  fgcl  22006  supfil  22023  ufinffr  22057  alexsubALTlem2  22176  metnrmlem3  22988  itg1addlem4  23803  uc1pval  24236  mon1pval  24238  pserulm  24513  vtxdun  26722  vtxdginducedm1  26784  difres  29921  imadifxp  29922  esumrnmpt2  30637  truae  30813  carsgclctunlem2  30888  derangsn  31660  poimirlem3  33892  ismblfin  33930  pcl0N  35934  pcl0bN  35935  coeq0i  38089  eldioph2lem2  38097  eldioph4b  38148  ntrk2imkb  39104  ntrk0kbimka  39106  ssin0  39969  iccdifprioo  40474  sumnnodd  40593  sge0split  41356  0setrec  43236