Theorem ss0b 4352

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

Step	Hyp	Ref	Expression
1		0ss 4351	. . 3 ⊢ ∅ ⊆ 𝐴
2		eqss 3949	. . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
3	1, 2	mpbiran2 720	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
4	3	bicomi 226	1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 208   = wceq 1559   ⊆ wss 3902  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-dif 3905  df-ss 3919  df-nul 4284

This theorem is referenced by:  ss0  4353  un00  4396  pw0  4767  al0ssb  5255  fnsuppeq0  8166  cnfcom2lem  9650  card0  9910  kmlem5  10105  cf0  10201  fin1a2lem12  10362  mreexexlem3d  17669  efgval  19748  ppttop  23055  0nnei  23160  bdayfinbndlem2  28549  disjunsn  32754  isarchi  33323  filnetlem4  36702  bj-pw0ALT  37495  coss0  39029  pnonsingN  40518  osumcllem4N  40544  resnonrel  44129  ntrneicls11  44627  ntrneikb  44631  sprsymrelfvlem  48057  isubgr0uhgr  48456  iuneq0  49401