Theorem ss0b 4358

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ⊆ wss 3905  ∅c0 4286

This proof depends on 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 proof 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 3908  df-ss 3922  df-nul 4287

This theorem is used by:  ss0  4359  sseq0b  4360  un00  4364  pw0  4778  al0ssb  5271  fnsuppeq0  8184  cnfcom2lem  9666  card0  9949  kmlem5  10143  cf0  10238  fin1a2lem12  10399  mreexexlem3d  17706  efgval  19791  ppttop  23173  0nnei  23278  bdayfinbndlem2  28670  disjunsn  32948  isarchi  33511  filnetlem4  36920  bj-pw0ALT  37713  coss0  39246  pnonsingN  40735  osumcllem4N  40761  resnonrel  44346  ntrneicls11  44844  ntrneikb  44848  sprsymrelfvlem  48267  isubgr0uhgr  48666  iuneq0  49625