Theorem ss0b 4424

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

Syntax hints:   ↔ wb 206   = wceq 1537   ⊆ wss 3976  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-dif 3979  df-ss 3993  df-nul 4353

This theorem is referenced by:  ss0  4425  un00  4468  pw0  4837  al0ssb  5326  fnsuppeq0  8233  cnfcom2lem  9770  card0  10027  kmlem5  10224  cf0  10320  fin1a2lem12  10480  mreexexlem3d  17704  efgval  19759  ppttop  23035  0nnei  23141  disjunsn  32616  isarchi  33162  filnetlem4  36347  bj-pw0ALT  37015  coss0  38435  pnonsingN  39890  osumcllem4N  39916  resnonrel  43554  ntrneicls11  44052  ntrneikb  44056  sprsymrelfvlem  47364  isubgr0uhgr  47743