Theorem ss0 4354

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3901  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3904  df-ss 3918  df-nul 4286

This theorem is referenced by:  sseq0  4355  0dif  4357  eq0rdvALT  4360  ssdisj  4412  disjpss  4413  dfopif  4826  iunxdif3  5050  fr0  5602  poirr2  6081  sofld  6145  f00  6716  fvmptopab  7413  tfindsg  7803  findsg  7839  frxp  8068  map0b  8821  sbthlem7  9021  ssfi  9097  fi0  9323  cantnflem1  9598  rankeq0b  9772  grur1a  10730  ixxdisj  13276  icodisj  13392  ioodisj  13398  uzdisj  13513  nn0disj  13560  hashf1lem2  14379  swrd0  14582  xptrrel  14903  sumz  15645  sumss  15647  fsum2dlem  15693  prod1  15867  prodss  15870  fprodss  15871  fprod2dlem  15903  cntzval  19250  oppglsm  19571  efgval  19646  islss  20885  00lss  20892  mplsubglem  21954  ntrcls0  23020  neindisj2  23067  hauscmplem  23350  fbdmn0  23778  fbncp  23783  opnfbas  23786  fbasfip  23812  fbunfip  23813  fgcl  23822  supfil  23839  ufinffr  23873  alexsubALTlem2  23992  metnrmlem3  24806  itg1addlem4  25656  uc1pval  26101  mon1pval  26103  pserulm  26387  vtxdun  29555  vtxdginducedm1  29617  difres  32675  imadifxp  32676  swrdrndisj  33039  cycpmco2f1  33206  erlval  33340  ssdifidllem  33537  ply1dg3rt0irred  33665  esumrnmpt2  34225  truae  34400  carsgclctunlem2  34476  acycgr0v  35342  prclisacycgr  35345  derangsn  35364  poimirlem3  37820  ismblfin  37858  pcl0N  40178  pcl0bN  40179  coeq0i  42991  eldioph2lem2  42999  eldioph4b  43049  oe0suclim  43515  ntrk2imkb  44274  ntrk0kbimka  44276  ssin0  45296  iccdifprioo  45758  sumnnodd  45872  sge0split  46649  iscnrm3llem2  49191  0setrec  49945