Theorem ss0 4365

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914  ∅c0 4296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-dif 3917  df-ss 3931  df-nul 4297

This theorem is referenced by:  sseq0  4366  0dif  4368  eq0rdvALT  4371  ssdisj  4423  disjpss  4424  dfopif  4834  iunxdif3  5059  fr0  5616  poirr2  6097  sofld  6160  f00  6742  fvmptopab  7443  tfindsg  7837  findsg  7873  frxp  8105  map0b  8856  sbthlem7  9057  ssfi  9137  fi0  9371  cantnflem1  9642  rankeq0b  9813  grur1a  10772  ixxdisj  13321  icodisj  13437  ioodisj  13443  uzdisj  13558  nn0disj  13605  hashf1lem2  14421  swrd0  14623  xptrrel  14946  sumz  15688  sumss  15690  fsum2dlem  15736  prod1  15910  prodss  15913  fprodss  15914  fprod2dlem  15946  cntzval  19253  oppglsm  19572  efgval  19647  islss  20840  00lss  20847  mplsubglem  21908  ntrcls0  22963  neindisj2  23010  hauscmplem  23293  fbdmn0  23721  fbncp  23726  opnfbas  23729  fbasfip  23755  fbunfip  23756  fgcl  23765  supfil  23782  ufinffr  23816  alexsubALTlem2  23935  metnrmlem3  24750  itg1addlem4  25600  uc1pval  26045  mon1pval  26047  pserulm  26331  vtxdun  29409  vtxdginducedm1  29471  difres  32529  imadifxp  32530  swrdrndisj  32879  cycpmco2f1  33081  erlval  33209  ssdifidllem  33427  ply1dg3rt0irred  33551  esumrnmpt2  34058  truae  34233  carsgclctunlem2  34310  acycgr0v  35135  prclisacycgr  35138  derangsn  35157  poimirlem3  37617  ismblfin  37655  pcl0N  39916  pcl0bN  39917  coeq0i  42741  eldioph2lem2  42749  eldioph4b  42799  oe0suclim  43266  ntrk2imkb  44026  ntrk0kbimka  44028  ssin0  45049  iccdifprioo  45514  sumnnodd  45628  sge0split  46407  iscnrm3llem2  48938  0setrec  49693