Theorem ss0b 4393

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 4392	. . 3 ⊢ ∅ ⊆ 𝐴
2		eqss 3993	. . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
3	1, 2	mpbiran2 708	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
4	3	bicomi 223	1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 205   = wceq 1541   ⊆ wss 3944  ∅c0 4318

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-dif 3947  df-in 3951  df-ss 3961  df-nul 4319

This theorem is referenced by:  ss0  4394  un00  4438  pw0  4808  al0ssb  5301  fnsuppeq0  8159  cnfcom2lem  9678  card0  9935  kmlem5  10131  cf0  10228  fin1a2lem12  10388  mreexexlem3d  17572  efgval  19549  ppttop  22439  0nnei  22545  disjunsn  31690  isarchi  32199  filnetlem4  35070  bj-pw0ALT  35734  coss0  37154  pnonsingN  38609  osumcllem4N  38635  resnonrel  42114  ntrneicls11  42612  ntrneikb  42616  sprsymrelfvlem  45930