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

Theorem ss0b 4354
 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 4353 . . 3 ∅ ⊆ 𝐴
2 eqss 3985 . . 3 (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
31, 2mpbiran2 706 . 2 (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
43bicomi 225 1 (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207   = wceq 1530   ⊆ wss 3939  ∅c0 4294 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-dif 3942  df-in 3946  df-ss 3955  df-nul 4295 This theorem is referenced by:  ss0  4355  un00  4396  pw0  4743  al0ssb  5208  fnsuppeq0  7852  cnfcom2lem  9156  card0  9379  kmlem5  9572  cf0  9665  fin1a2lem12  9825  mreexexlem3d  16909  efgval  18765  ppttop  21531  0nnei  21636  disjunsn  30260  isarchi  30726  filnetlem4  33614  coss0  35587  pnonsingN  36937  osumcllem4N  36963  resnonrel  39814  ntrneicls11  40302  ntrneikb  40306  sprsymrelfvlem  43481
 Copyright terms: Public domain W3C validator