Theorem ss0b 4367

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 4366	. . 3 ⊢ ∅ ⊆ 𝐴
2		eqss 3965	. . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
3	1, 2	mpbiran2 710	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
4	3	bicomi 224	1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 206   = wceq 1540   ⊆ wss 3917  ∅c0 4299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-dif 3920  df-ss 3934  df-nul 4300

This theorem is referenced by:  ss0  4368  un00  4411  pw0  4779  al0ssb  5266  fnsuppeq0  8174  cnfcom2lem  9661  card0  9918  kmlem5  10115  cf0  10211  fin1a2lem12  10371  mreexexlem3d  17614  efgval  19654  ppttop  22901  0nnei  23006  disjunsn  32530  isarchi  33143  filnetlem4  36376  bj-pw0ALT  37044  coss0  38477  pnonsingN  39934  osumcllem4N  39960  resnonrel  43588  ntrneicls11  44086  ntrneikb  44090  sprsymrelfvlem  47495  isubgr0uhgr  47877  iuneq0  48811