Theorem ss0b 4395

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 4394	. . 3 ⊢ ∅ ⊆ 𝐴
2		eqss 3994	. . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
3	1, 2	mpbiran2 708	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
4	3	bicomi 223	1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 205   = wceq 1534   ⊆ wss 3946  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-dif 3949  df-ss 3963  df-nul 4323

This theorem is referenced by:  ss0  4396  un00  4439  pw0  4811  al0ssb  5305  fnsuppeq0  8198  cnfcom2lem  9737  card0  9994  kmlem5  10190  cf0  10285  fin1a2lem12  10445  mreexexlem3d  17654  efgval  19711  ppttop  22998  0nnei  23104  disjunsn  32514  isarchi  33051  filnetlem4  36106  bj-pw0ALT  36769  coss0  38190  pnonsingN  39645  osumcllem4N  39671  resnonrel  43296  ntrneicls11  43794  ntrneikb  43798  sprsymrelfvlem  47098  isubgr0uhgr  47474