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

Theorem ss0b 3925
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 3924 . . 3 ∅ ⊆ 𝐴
2 eqss 3583 . . 3 (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
31, 2mpbiran2 956 . 2 (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
43bicomi 213 1 (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  wb 195   = wceq 1475  wss 3540  c0 3874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875
This theorem is referenced by:  ss0  3926  un00  3963  ssdisjOLD  3979  pw0  4283  fnsuppeq0  7210  cnfcom2lem  8481  card0  8667  kmlem5  8859  cf0  8956  fin1a2lem12  9116  mreexexlem3d  16129  efgval  17953  ppttop  20621  0nnei  20726  disjunsn  28789  isarchi  29067  filnetlem4  31546  pnonsingN  34237  osumcllem4N  34263  resnonrel  36917  ntrneicls11  37408  ntrneikb  37412
  Copyright terms: Public domain W3C validator