Theorem ss0b 4359

Description: Any subset of the empty set is empty. Dual of vss 4366. 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 4358	. . 3 ⊢ ∅ ⊆ 𝐴
2		eqss 3953	. . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
3	1, 2	mpbiran2 722	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
4	3	bicomi 227	1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 209   = wceq 1570   ⊆ wss 3906  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-dif 3909  df-ss 3923  df-nul 4288

This theorem is referenced by:  ss0  4360  sseq0b  4361  un00  4365  pw0  4779  al0ssb  5272  fnsuppeq0  8189  cnfcom2lem  9671  card0  9945  kmlem5  10139  cf0  10235  fin1a2lem12  10396  mreexexlem3d  17703  efgval  19788  ppttop  23145  0nnei  23250  bdayfinbndlem2  28642  disjunsn  32920  isarchi  33483  filnetlem4  36873  bj-pw0ALT  37666  coss0  39199  pnonsingN  40688  osumcllem4N  40714  resnonrel  44301  ntrneicls11  44799  ntrneikb  44803  sprsymrelfvlem  48222  isubgr0uhgr  48621  iuneq0  49580