Theorem ss0b 4350

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

Syntax hints:   ↔ wb 206   = wceq 1541   ⊆ wss 3898  ∅c0 4282

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-dif 3901  df-ss 3915  df-nul 4283

This theorem is referenced by:  ss0  4351  un00  4394  pw0  4765  al0ssb  5250  fnsuppeq0  8131  cnfcom2lem  9602  card0  9862  kmlem5  10057  cf0  10153  fin1a2lem12  10313  mreexexlem3d  17560  efgval  19637  ppttop  22942  0nnei  23047  disjunsn  32595  isarchi  33192  filnetlem4  36497  bj-pw0ALT  37166  coss0  38654  pnonsingN  40105  osumcllem4N  40131  resnonrel  43749  ntrneicls11  44247  ntrneikb  44251  sprsymrelfvlem  47652  isubgr0uhgr  48035  iuneq0  48980