Theorem ss0 3461

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

Syntax hints:   → wi 4   = wceq 1353   ⊆ wss 3127  ∅c0 3420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-dif 3129  df-in 3133  df-ss 3140  df-nul 3421

This theorem is referenced by:  sseq0  3462  abf  3464  eq0rdv  3465  ssdisj  3477  0dif  3492  poirr2  5013  iotanul  5185  f00  5399  map0b  6677  phplem2  6843  php5dom  6853  sbthlem7  6952  fi0  6964  casefun  7074  caseinj  7078  djufun  7093  djuinj  7095  nnnninfeq  7116  exmidomni  7130  ixxdisj  9874  icodisj  9963  ioodisj  9964  uzdisj  10063  nn0disj  10108  fsum2dlemstep  11410  fprodssdc  11566  fprod2dlemstep  11598  ntrcls0  13211