Theorem ss0b 4355

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

Syntax hints:   ↔ wb 206   = wceq 1542   ⊆ wss 3903  ∅c0 4287

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-dif 3906  df-ss 3920  df-nul 4288

This theorem is referenced by:  ss0  4356  un00  4399  pw0  4770  al0ssb  5255  fnsuppeq0  8144  cnfcom2lem  9622  card0  9882  kmlem5  10077  cf0  10173  fin1a2lem12  10333  mreexexlem3d  17581  efgval  19658  ppttop  22963  0nnei  23068  bdayfinbndlem2  28476  disjunsn  32680  isarchi  33275  filnetlem4  36594  bj-pw0ALT  37294  coss0  38817  pnonsingN  40306  osumcllem4N  40332  resnonrel  43945  ntrneicls11  44443  ntrneikb  44447  sprsymrelfvlem  47847  isubgr0uhgr  48230  iuneq0  49175