Theorem ss0 4399

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3949  ∅c0 4323

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 3952  df-in 3956  df-ss 3966  df-nul 4324

This theorem is referenced by:  sseq0  4400  0dif  4402  eq0rdvALT  4406  ssdisj  4460  disjpss  4461  dfopif  4871  iunxdif3  5099  fr0  5656  poirr2  6126  sofld  6187  f00  6774  fvmptopab  7463  tfindsg  7850  findsg  7890  frxp  8112  map0b  8877  sbthlem7  9089  ssfi  9173  phplem2OLD  9218  fi0  9415  cantnflem1  9684  rankeq0b  9855  grur1a  10814  ixxdisj  13339  icodisj  13453  ioodisj  13459  uzdisj  13574  nn0disj  13617  hashf1lem2  14417  swrd0  14608  xptrrel  14927  sumz  15668  sumss  15670  fsum2dlem  15716  prod1  15888  prodss  15891  fprodss  15892  fprod2dlem  15924  cntzval  19185  oppglsm  19510  efgval  19585  islss  20545  00lss  20552  mplsubglem  21558  ntrcls0  22580  neindisj2  22627  hauscmplem  22910  fbdmn0  23338  fbncp  23343  opnfbas  23346  fbasfip  23372  fbunfip  23373  fgcl  23382  supfil  23399  ufinffr  23433  alexsubALTlem2  23552  metnrmlem3  24377  itg1addlem4  25216  itg1addlem4OLD  25217  uc1pval  25657  mon1pval  25659  pserulm  25934  vtxdun  28738  vtxdginducedm1  28800  difres  31831  imadifxp  31832  swrdrndisj  32121  cycpmco2f1  32283  esumrnmpt2  33066  truae  33241  carsgclctunlem2  33318  acycgr0v  34139  prclisacycgr  34142  derangsn  34161  poimirlem3  36491  ismblfin  36529  pcl0N  38793  pcl0bN  38794  coeq0i  41491  eldioph2lem2  41499  eldioph4b  41549  oe0suclim  42027  ntrk2imkb  42788  ntrk0kbimka  42790  ssin0  43742  iccdifprioo  44229  sumnnodd  44346  sge0split  45125  iscnrm3llem2  47583  0setrec  47749