Theorem ss0 4356

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-dif 3906  df-ss 3920  df-nul 4288

This theorem is referenced by:  sseq0  4357  0dif  4359  eq0rdvALT  4362  ssdisj  4414  disjpss  4415  dfopif  4828  iunxdif3  5052  fr0  5610  poirr2  6089  sofld  6153  f00  6724  fvmptopab  7423  tfindsg  7813  findsg  7849  frxp  8078  map0b  8833  sbthlem7  9033  ssfi  9109  fi0  9335  cantnflem1  9610  rankeq0b  9784  grur1a  10742  ixxdisj  13288  icodisj  13404  ioodisj  13410  uzdisj  13525  nn0disj  13572  hashf1lem2  14391  swrd0  14594  xptrrel  14915  sumz  15657  sumss  15659  fsum2dlem  15705  prod1  15879  prodss  15882  fprodss  15883  fprod2dlem  15915  cntzval  19262  oppglsm  19583  efgval  19658  islss  20897  00lss  20904  mplsubglem  21966  ntrcls0  23032  neindisj2  23079  hauscmplem  23362  fbdmn0  23790  fbncp  23795  opnfbas  23798  fbasfip  23824  fbunfip  23825  fgcl  23834  supfil  23851  ufinffr  23885  alexsubALTlem2  24004  metnrmlem3  24818  itg1addlem4  25668  uc1pval  26113  mon1pval  26115  pserulm  26399  vtxdun  29567  vtxdginducedm1  29629  difres  32686  imadifxp  32687  swrdrndisj  33049  cycpmco2f1  33217  erlval  33351  ssdifidllem  33548  ply1dg3rt0irred  33676  esumrnmpt2  34245  truae  34420  carsgclctunlem2  34496  acycgr0v  35361  prclisacycgr  35364  derangsn  35383  poimirlem3  37868  ismblfin  37906  pcl0N  40292  pcl0bN  40293  coeq0i  43104  eldioph2lem2  43112  eldioph4b  43162  oe0suclim  43628  ntrk2imkb  44387  ntrk0kbimka  44389  ssin0  45409  iccdifprioo  45870  sumnnodd  45984  sge0split  46761  iscnrm3llem2  49303  0setrec  50057