Theorem ss0b 4407

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

Syntax hints:   ↔ wb 206   = wceq 1537   ⊆ wss 3963  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-dif 3966  df-ss 3980  df-nul 4340

This theorem is referenced by:  ss0  4408  un00  4451  pw0  4817  al0ssb  5314  fnsuppeq0  8216  cnfcom2lem  9739  card0  9996  kmlem5  10193  cf0  10289  fin1a2lem12  10449  mreexexlem3d  17691  efgval  19750  ppttop  23030  0nnei  23136  disjunsn  32614  isarchi  33172  filnetlem4  36364  bj-pw0ALT  37032  coss0  38461  pnonsingN  39916  osumcllem4N  39942  resnonrel  43582  ntrneicls11  44080  ntrneikb  44084  sprsymrelfvlem  47415  isubgr0uhgr  47797