Theorem ss0b 4328

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 4327	. . 3 ⊢ ∅ ⊆ 𝐴
2		eqss 3932	. . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
3	1, 2	mpbiran2 706	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
4	3	bicomi 223	1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 205   = wceq 1539   ⊆ wss 3883  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900  df-nul 4254

This theorem is referenced by:  ss0  4329  un00  4373  pw0  4742  al0ssb  5227  fnsuppeq0  7979  cnfcom2lem  9389  card0  9647  kmlem5  9841  cf0  9938  fin1a2lem12  10098  mreexexlem3d  17272  efgval  19238  ppttop  22065  0nnei  22171  disjunsn  30834  isarchi  31338  filnetlem4  34497  bj-pw0ALT  35149  coss0  36524  pnonsingN  37874  osumcllem4N  37900  resnonrel  41089  ntrneicls11  41589  ntrneikb  41593  sprsymrelfvlem  44830