Theorem ss0b 4329

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 4328	. . 3 ⊢ ∅ ⊆ 𝐴
2		eqss 3930	. . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
3	1, 2	mpbiran2 716	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
4	3	bicomi 225	1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 207   = wceq 1547   ⊆ wss 3883  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-dif 3886  df-ss 3900  df-nul 4262

This theorem is referenced by:  ss0  4330  un00  4373  pw0  4743  al0ssb  5230  fnsuppeq0  8132  cnfcom2lem  9613  card0  9873  kmlem5  10068  cf0  10164  fin1a2lem12  10324  mreexexlem3d  17603  efgval  19683  ppttop  22990  0nnei  23095  bdayfinbndlem2  28478  disjunsn  32683  isarchi  33263  filnetlem4  36609  bj-pw0ALT  37402  coss0  38936  pnonsingN  40425  osumcllem4N  40451  resnonrel  44036  ntrneicls11  44534  ntrneikb  44538  sprsymrelfvlem  47965  isubgr0uhgr  48364  iuneq0  49309