Theorem ss0b 4342

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 4341	. . 3 ⊢ ∅ ⊆ 𝐴
2		eqss 3938	. . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
3	1, 2	mpbiran2 711	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
4	3	bicomi 224	1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 206   = wceq 1542   ⊆ wss 3890  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-dif 3893  df-ss 3907  df-nul 4275

This theorem is referenced by:  ss0  4343  un00  4386  pw0  4756  al0ssb  5243  fnsuppeq0  8135  cnfcom2lem  9613  card0  9873  kmlem5  10068  cf0  10164  fin1a2lem12  10324  mreexexlem3d  17603  efgval  19683  ppttop  22982  0nnei  23087  bdayfinbndlem2  28474  disjunsn  32679  isarchi  33258  filnetlem4  36579  bj-pw0ALT  37372  coss0  38904  pnonsingN  40393  osumcllem4N  40419  resnonrel  44037  ntrneicls11  44535  ntrneikb  44539  sprsymrelfvlem  47962  isubgr0uhgr  48361  iuneq0  49306