Theorem ss0b 4287

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

Syntax hints:   ↔ wb 209   = wceq 1542   ⊆ wss 3844  ∅c0 4212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3401  df-dif 3847  df-in 3851  df-ss 3861  df-nul 4213

This theorem is referenced by:  ss0  4288  un00  4333  pw0  4701  al0ssb  5177  fnsuppeq0  7890  cnfcom2lem  9240  card0  9463  kmlem5  9657  cf0  9754  fin1a2lem12  9914  mreexexlem3d  17023  efgval  18964  ppttop  21761  0nnei  21866  disjunsn  30510  isarchi  31016  filnetlem4  34216  bj-pw0ALT  34868  coss0  36243  pnonsingN  37593  osumcllem4N  37619  resnonrel  40768  ntrneicls11  41269  ntrneikb  41273  sprsymrelfvlem  44506