Theorem ss0b 4364

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 4363	. . 3 ⊢ ∅ ⊆ 𝐴
2		eqss 3960	. . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
3	1, 2	mpbiran2 722	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
4	3	bicomi 227	1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 209   = wceq 1567   ⊆ wss 3913  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-dif 3916  df-ss 3930  df-nul 4295

This theorem is referenced by:  ss0  4365  un00  4408  pw0  4779  al0ssb  5270  fnsuppeq0  8184  cnfcom2lem  9666  card0  9940  kmlem5  10134  cf0  10230  fin1a2lem12  10391  mreexexlem3d  17698  efgval  19783  ppttop  23129  0nnei  23234  bdayfinbndlem2  28623  disjunsn  32876  isarchi  33439  filnetlem4  36777  bj-pw0ALT  37569  coss0  39103  pnonsingN  40592  osumcllem4N  40618  resnonrel  44203  ntrneicls11  44701  ntrneikb  44705  sprsymrelfvlem  48121  isubgr0uhgr  48520  iuneq0  49475