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

Theorem ss0b 4081
 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 4080 . . 3 ∅ ⊆ 𝐴
2 eqss 3724 . . 3 (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
31, 2mpbiran2 992 . 2 (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
43bicomi 214 1 (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   = wceq 1596   ⊆ wss 3680  ∅c0 4023 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-dif 3683  df-in 3687  df-ss 3694  df-nul 4024 This theorem is referenced by:  ss0  4082  un00  4119  ssdisjOLD  4135  pw0  4451  fnsuppeq0  7443  cnfcom2lem  8711  card0  8897  kmlem5  9089  cf0  9186  fin1a2lem12  9346  mreexexlem3d  16429  efgval  18251  ppttop  20934  0nnei  21039  disjunsn  29635  isarchi  29966  filnetlem4  32603  coss0  34471  pnonsingN  35639  osumcllem4N  35665  resnonrel  38317  ntrneicls11  38807  ntrneikb  38811  sprsymrelfvlem  42167
 Copyright terms: Public domain W3C validator