Theorem ss0 4397

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3947  ∅c0 4321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3950  df-in 3954  df-ss 3964  df-nul 4322

This theorem is referenced by:  sseq0  4398  0dif  4400  eq0rdvALT  4404  ssdisj  4458  disjpss  4459  dfopif  4869  iunxdif3  5097  fr0  5654  poirr2  6122  sofld  6183  f00  6770  fvmptopab  7458  tfindsg  7845  findsg  7885  frxp  8107  map0b  8873  sbthlem7  9085  ssfi  9169  phplem2OLD  9214  fi0  9411  cantnflem1  9680  rankeq0b  9851  grur1a  10810  ixxdisj  13335  icodisj  13449  ioodisj  13455  uzdisj  13570  nn0disj  13613  hashf1lem2  14413  swrd0  14604  xptrrel  14923  sumz  15664  sumss  15666  fsum2dlem  15712  prod1  15884  prodss  15887  fprodss  15888  fprod2dlem  15920  cntzval  19179  oppglsm  19503  efgval  19578  islss  20533  00lss  20540  mplsubglem  21540  ntrcls0  22562  neindisj2  22609  hauscmplem  22892  fbdmn0  23320  fbncp  23325  opnfbas  23328  fbasfip  23354  fbunfip  23355  fgcl  23364  supfil  23381  ufinffr  23415  alexsubALTlem2  23534  metnrmlem3  24359  itg1addlem4  25198  itg1addlem4OLD  25199  uc1pval  25639  mon1pval  25641  pserulm  25916  vtxdun  28718  vtxdginducedm1  28780  difres  31809  imadifxp  31810  swrdrndisj  32099  cycpmco2f1  32261  esumrnmpt2  33004  truae  33179  carsgclctunlem2  33256  acycgr0v  34077  prclisacycgr  34080  derangsn  34099  poimirlem3  36429  ismblfin  36467  pcl0N  38731  pcl0bN  38732  coeq0i  41424  eldioph2lem2  41432  eldioph4b  41482  oe0suclim  41960  ntrk2imkb  42721  ntrk0kbimka  42723  ssin0  43675  iccdifprioo  44164  sumnnodd  44281  sge0split  45060  iscnrm3llem2  47485  0setrec  47651