Theorem ss0b 4081

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

Syntax hints:   ↔ wb 196   = wceq 1596   ⊆ wss 3680  ∅c0 4023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-dif 3683  df-in 3687  df-ss 3694  df-nul 4024

This theorem is referenced by:  ss0  4082  un00  4119  ssdisjOLD  4135  pw0  4451  fnsuppeq0  7443  cnfcom2lem  8711  card0  8897  kmlem5  9089  cf0  9186  fin1a2lem12  9346  mreexexlem3d  16429  efgval  18251  ppttop  20934  0nnei  21039  disjunsn  29635  isarchi  29966  filnetlem4  32603  coss0  34471  pnonsingN  35639  osumcllem4N  35665  resnonrel  38317  ntrneicls11  38807  ntrneikb  38811  sprsymrelfvlem  42167