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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-dif 3909  df-ss 3923  df-nul 4287

This theorem is used by:  ss0  4359  sseq0b  4360  un00  4364  pw0  4780  al0ssb  5273  fnsuppeq0  8190  cnfcom2lem  9673  card0  9956  kmlem5  10150  cf0  10245  fin1a2lem12  10406  mreexexlem3d  17719  efgval  19810  ppttop  23193  0nnei  23298  bdayfinbndlem2  28690  disjunsn  32968  isarchi  33525  filnetlem4  36925  bj-pw0ALT  37718  coss0  39251  pnonsingN  40740  osumcllem4N  40766  resnonrel  44351  ntrneicls11  44849  ntrneikb  44853  sprsymrelfvlem  48272  isubgr0uhgr  48671  iuneq0  49630