Theorem ss0b 4353

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

Syntax hints:   ↔ wb 206   = wceq 1541   ⊆ wss 3901  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3904  df-ss 3918  df-nul 4286

This theorem is referenced by:  ss0  4354  un00  4397  pw0  4768  al0ssb  5253  fnsuppeq0  8134  cnfcom2lem  9610  card0  9870  kmlem5  10065  cf0  10161  fin1a2lem12  10321  mreexexlem3d  17569  efgval  19646  ppttop  22951  0nnei  23056  bdayfinbndlem2  28464  disjunsn  32669  isarchi  33264  filnetlem4  36575  bj-pw0ALT  37250  coss0  38742  pnonsingN  40193  osumcllem4N  40219  resnonrel  43833  ntrneicls11  44331  ntrneikb  44335  sprsymrelfvlem  47736  isubgr0uhgr  48119  iuneq0  49064