Theorem ss0b 4351

Description: Any subset of the empty set is empty. Dual of vss 4358. 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 4350	. . 3 ⊢ ∅ ⊆ 𝐴
2		eqss 3946	. . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
3	1, 2	mpbiran2 723	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
4	3	bicomi 227	1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)

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

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-dif 3902  df-ss 3916  df-nul 4280

This theorem is used by:  ss0  4352  sseq0b  4353  un00  4357  pw0  4773  al0ssb  5265  fnsuppeq0  8190  cnfcom2lem  9680  card0  9963  kmlem5  10157  cf0  10252  fin1a2lem12  10413  mreexexlem3d  17734  efgval  19844  ppttop  23232  0nnei  23337  bdayfinbndlem2  28733  disjunsn  33067  isarchi  33622  filnetlem4  37000  bj-pw0ALT  37793  coss0  39317  pnonsingN  40806  osumcllem4N  40832  resnonrel  44432  ntrneicls11  44930  ntrneikb  44934  sprsymrelfvlem  48390  isubgr0uhgr  48789  iuneq0  49747