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 2733

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 2740  df-cleq 2753  df-clel 2836  df-dif 3902  df-ss 3916  df-nul 4280

This theorem is used by:  ss0  4352  sseq0b  4353  un00  4357  pw0  4773  al0ssb  5262  fnsuppeq0  8202  cnfcom2lem  9695  card0  10032  kmlem5  10226  cf0  10321  fin1a2lem12  10482  mreexexlem3d  17813  efgval  19924  ppttop  23318  0nnei  23423  bdayfinbndlem2  28847  disjunsn  33181  isarchi  33736  filnetlem4  37149  bj-pw0ALT  37944  coss0  39481  pnonsingN  40970  osumcllem4N  40996  resnonrel  44577  ntrneicls11  45075  ntrneikb  45079  sprsymrelfvlem  48541  isubgr0uhgr  48940  iuneq0  49898