Theorem ss0b 4397

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

Syntax hints:   ↔ wb 205   = wceq 1541   ⊆ wss 3948  ∅c0 4322

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951  df-in 3955  df-ss 3965  df-nul 4323

This theorem is referenced by:  ss0  4398  un00  4442  pw0  4815  al0ssb  5308  fnsuppeq0  8176  cnfcom2lem  9695  card0  9952  kmlem5  10148  cf0  10245  fin1a2lem12  10405  mreexexlem3d  17589  efgval  19584  ppttop  22509  0nnei  22615  disjunsn  31820  isarchi  32323  filnetlem4  35261  bj-pw0ALT  35925  coss0  37344  pnonsingN  38799  osumcllem4N  38825  resnonrel  42333  ntrneicls11  42831  ntrneikb  42835  sprsymrelfvlem  46148