Theorem ss0 4377

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3926  ∅c0 4308

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-dif 3929  df-ss 3943  df-nul 4309

This theorem is referenced by:  sseq0  4378  0dif  4380  eq0rdvALT  4383  ssdisj  4435  disjpss  4436  dfopif  4846  iunxdif3  5071  fr0  5632  poirr2  6113  sofld  6176  f00  6760  fvmptopab  7461  tfindsg  7856  findsg  7893  frxp  8125  map0b  8897  sbthlem7  9103  ssfi  9187  phplem2OLD  9229  fi0  9432  cantnflem1  9703  rankeq0b  9874  grur1a  10833  ixxdisj  13377  icodisj  13493  ioodisj  13499  uzdisj  13614  nn0disj  13661  hashf1lem2  14474  swrd0  14676  xptrrel  14999  sumz  15738  sumss  15740  fsum2dlem  15786  prod1  15960  prodss  15963  fprodss  15964  fprod2dlem  15996  cntzval  19304  oppglsm  19623  efgval  19698  islss  20891  00lss  20898  mplsubglem  21959  ntrcls0  23014  neindisj2  23061  hauscmplem  23344  fbdmn0  23772  fbncp  23777  opnfbas  23780  fbasfip  23806  fbunfip  23807  fgcl  23816  supfil  23833  ufinffr  23867  alexsubALTlem2  23986  metnrmlem3  24801  itg1addlem4  25652  uc1pval  26097  mon1pval  26099  pserulm  26383  vtxdun  29461  vtxdginducedm1  29523  difres  32581  imadifxp  32582  swrdrndisj  32933  cycpmco2f1  33135  erlval  33253  ssdifidllem  33471  ply1dg3rt0irred  33595  esumrnmpt2  34099  truae  34274  carsgclctunlem2  34351  acycgr0v  35170  prclisacycgr  35173  derangsn  35192  poimirlem3  37647  ismblfin  37685  pcl0N  39941  pcl0bN  39942  coeq0i  42776  eldioph2lem2  42784  eldioph4b  42834  oe0suclim  43301  ntrk2imkb  44061  ntrk0kbimka  44063  ssin0  45079  iccdifprioo  45545  sumnnodd  45659  sge0split  46438  iscnrm3llem2  48924  0setrec  49568