Theorem ss0 3926

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

Syntax hints:   → wi 4   = wceq 1475   ⊆ wss 3540  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875

This theorem is referenced by:  sseq0  3927  0dif  3929  eq0rdv  3931  ssdisj  3978  ssdisjOLD  3979  disjpss  3980  dfopif  4337  iunxdif3  4542  fr0  5017  poirr2  5439  sofld  5500  f00  6000  tfindsg  6952  findsg  6985  frxp  7174  map0b  7782  sbthlem7  7961  phplem2  8025  fi0  8209  cantnflem1  8469  rankeq0b  8606  grur1a  9520  ixxdisj  12061  icodisj  12168  ioodisj  12173  uzdisj  12282  nn0disj  12324  hashf1lem2  13097  swrd0  13286  xptrrel  13567  sumz  14300  sumss  14302  fsum2dlem  14343  prod1  14513  prodss  14516  fprodss  14517  fprod2dlem  14549  cntzval  17577  symgbas  17623  oppglsm  17880  efgval  17953  islss  18756  00lss  18763  mplsubglem  19255  ntrcls0  20690  neindisj2  20737  hauscmplem  21019  fbdmn0  21448  fbncp  21453  opnfbas  21456  fbasfip  21482  fbunfip  21483  fgcl  21492  supfil  21509  ufinffr  21543  alexsubALTlem2  21662  metnrmlem3  22472  itg1addlem4  23272  uc1pval  23703  mon1pval  23705  pserulm  23980  vdgrun  26428  vdgrfiun  26429  difres  28795  imadifxp  28796  esumrnmpt2  29457  truae  29633  carsgclctunlem2  29708  derangsn  30406  poimirlem3  32582  ismblfin  32620  pcl0N  34226  pcl0bN  34227  coeq0i  36334  eldioph2lem2  36342  eldioph4b  36393  ntrk2imkb  37355  ntrk0kbimka  37357  ssin0  38248  iccdifprioo  38589  sumnnodd  38697  sge0split  39302  vtxdun  40696  0setrec  42246