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

Theorem ss0b 3924
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 3923 . . 3 ∅ ⊆ 𝐴
2 eqss 3582 . . 3 (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
31, 2mpbiran2 955 . 2 (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
43bicomi 212 1 (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wss 3539  c0 3873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542  df-in 3546  df-ss 3553  df-nul 3874
This theorem is referenced by:  ss0  3925  un00  3962  ssdisjOLD  3978  pw0  4282  fnsuppeq0  7187  cnfcom2lem  8458  card0  8644  kmlem5  8836  cf0  8933  fin1a2lem12  9093  mreexexlem3d  16075  efgval  17899  ppttop  20563  0nnei  20668  disjunsn  28595  isarchi  28873  filnetlem4  31352  pnonsingN  34040  osumcllem4N  34066  resnonrel  36720  ntrneicls11  37211  ntrneikb  37215
  Copyright terms: Public domain W3C validator