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

Theorem ss0b 4393
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 4392 . . 3 ∅ ⊆ 𝐴
2 eqss 3993 . . 3 (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
31, 2mpbiran2 708 . 2 (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
43bicomi 223 1 (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1541  wss 3944  c0 4318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-dif 3947  df-in 3951  df-ss 3961  df-nul 4319
This theorem is referenced by:  ss0  4394  un00  4438  pw0  4808  al0ssb  5301  fnsuppeq0  8159  cnfcom2lem  9678  card0  9935  kmlem5  10131  cf0  10228  fin1a2lem12  10388  mreexexlem3d  17572  efgval  19549  ppttop  22439  0nnei  22545  disjunsn  31690  isarchi  32199  filnetlem4  35070  bj-pw0ALT  35734  coss0  37154  pnonsingN  38609  osumcllem4N  38635  resnonrel  42114  ntrneicls11  42612  ntrneikb  42616  sprsymrelfvlem  45930
  Copyright terms: Public domain W3C validator