Theorem ss0b 4305

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

Syntax hints:   ↔ wb 209   = wceq 1538   ⊆ wss 3881  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244

This theorem is referenced by:  ss0  4306  un00  4350  pw0  4705  al0ssb  5176  fnsuppeq0  7841  cnfcom2lem  9148  card0  9371  kmlem5  9565  cf0  9662  fin1a2lem12  9822  mreexexlem3d  16909  efgval  18835  ppttop  21612  0nnei  21717  disjunsn  30357  isarchi  30861  filnetlem4  33842  bj-pw0ALT  34466  coss0  35879  pnonsingN  37229  osumcllem4N  37255  resnonrel  40292  ntrneicls11  40793  ntrneikb  40797  sprsymrelfvlem  44007