Theorem ss0 4109

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

Syntax hints:   → wi 4   = wceq 1624   ⊆ wss 3707  ∅c0 4050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-dif 3710  df-in 3714  df-ss 3721  df-nul 4051

This theorem is referenced by:  sseq0  4110  0dif  4112  eq0rdv  4114  ssdisj  4162  ssdisjOLD  4163  disjpss  4164  dfopif  4542  iunxdif3  4750  fr0  5237  poirr2  5670  sofld  5731  f00  6240  tfindsg  7217  findsg  7250  frxp  7447  map0b  8054  sbthlem7  8233  phplem2  8297  fi0  8483  cantnflem1  8751  rankeq0b  8888  grur1a  9825  ixxdisj  12375  icodisj  12482  ioodisj  12487  uzdisj  12598  nn0disj  12641  hashf1lem2  13424  swrd0  13626  xptrrel  13912  sumz  14644  sumss  14646  fsum2dlem  14692  prod1  14865  prodss  14868  fprodss  14869  fprod2dlem  14901  cntzval  17946  symgbas  17992  oppglsm  18249  efgval  18322  islss  19129  00lss  19136  mplsubglem  19628  ntrcls0  21074  neindisj2  21121  hauscmplem  21403  fbdmn0  21831  fbncp  21836  opnfbas  21839  fbasfip  21865  fbunfip  21866  fgcl  21875  supfil  21892  ufinffr  21926  alexsubALTlem2  22045  metnrmlem3  22857  itg1addlem4  23657  uc1pval  24090  mon1pval  24092  pserulm  24367  vtxdun  26579  vtxdginducedm1  26641  difres  29712  imadifxp  29713  esumrnmpt2  30431  truae  30607  carsgclctunlem2  30682  derangsn  31451  poimirlem3  33717  ismblfin  33755  pcl0N  35703  pcl0bN  35704  coeq0i  37810  eldioph2lem2  37818  eldioph4b  37869  ntrk2imkb  38829  ntrk0kbimka  38831  ssin0  39714  iccdifprioo  40237  sumnnodd  40357  sge0split  41121  0setrec  42952