MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ss0b Structured version   Visualization version   GIF version

Theorem ss0b 4395
Description: Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its converse. (Contributed by NM, 17-Sep-2003.)
Assertion
Ref Expression
ss0b (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)

Proof of Theorem ss0b
StepHypRef Expression
1 0ss 4394 . . 3 ∅ ⊆ 𝐴
2 eqss 3994 . . 3 (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
31, 2mpbiran2 708 . 2 (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
43bicomi 223 1 (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1534  wss 3946  c0 4322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-dif 3949  df-ss 3963  df-nul 4323
This theorem is referenced by:  ss0  4396  un00  4439  pw0  4811  al0ssb  5305  fnsuppeq0  8198  cnfcom2lem  9737  card0  9994  kmlem5  10190  cf0  10285  fin1a2lem12  10445  mreexexlem3d  17654  efgval  19711  ppttop  22998  0nnei  23104  disjunsn  32514  isarchi  33051  filnetlem4  36106  bj-pw0ALT  36769  coss0  38190  pnonsingN  39645  osumcllem4N  39671  resnonrel  43296  ntrneicls11  43794  ntrneikb  43798  sprsymrelfvlem  47098  isubgr0uhgr  47474
  Copyright terms: Public domain W3C validator