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

Theorem ss0b 4169
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 4168 . . 3 ∅ ⊆ 𝐴
2 eqss 3813 . . 3 (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
31, 2mpbiran2 702 . 2 (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
43bicomi 216 1 (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wb 198   = wceq 1653  wss 3769  c0 4115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-v 3387  df-dif 3772  df-in 3776  df-ss 3783  df-nul 4116
This theorem is referenced by:  ss0  4170  un00  4207  pw0  4531  al0ssb  4985  fnsuppeq0  7561  cnfcom2lem  8848  card0  9070  kmlem5  9264  cf0  9361  fin1a2lem12  9521  mreexexlem3d  16621  efgval  18443  ppttop  21140  0nnei  21245  disjunsn  29924  isarchi  30252  filnetlem4  32888  coss0  34723  pnonsingN  35954  osumcllem4N  35980  resnonrel  38681  ntrneicls11  39170  ntrneikb  39174  sprsymrelfvlem  42539
  Copyright terms: Public domain W3C validator