Theorem ss0b 4350

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ⊆ wss 3895  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-dif 4047  df-nul 4279

This theorem is used by:  ss0  4351  sseq0b  4352  un00  4356  pw0  4829  al0ssb  5261  fnsuppeq0  8213  cnfcom2lem  9706  card0  10043  kmlem5  10237  cf0  10332  fin1a2lem12  10493  mreexexlem3d  17826  efgval  19937  ppttop  23331  0nnei  23436  bdayfinbndlem2  28860  disjunsn  33236  isarchi  33790  filnetlem4  37262  bj-pw0ALT  38057  coss0  39595  pnonsingN  41084  osumcllem4N  41110  resnonrel  44686  ntrneicls11  45184  ntrneikb  45188  sprsymrelfvlem  48666  isubgr0uhgr  49065  iuneq0  50024