Theorem ss0b 3973

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 3972	. . 3 ⊢ ∅ ⊆ 𝐴
2		eqss 3618	. . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
3	1, 2	mpbiran2 954	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
4	3	bicomi 214	1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 196   = wceq 1483   ⊆ wss 3574  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916

This theorem is referenced by:  ss0  3974  un00  4011  ssdisjOLD  4027  pw0  4343  fnsuppeq0  7323  cnfcom2lem  8598  card0  8784  kmlem5  8976  cf0  9073  fin1a2lem12  9233  mreexexlem3d  16306  efgval  18130  ppttop  20811  0nnei  20916  disjunsn  29407  isarchi  29736  filnetlem4  32376  pnonsingN  35219  osumcllem4N  35245  resnonrel  37898  ntrneicls11  38388  ntrneikb  38392  sprsymrelfvlem  41740