Theorem ss0b 4169

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 4168	. . 3 ⊢ ∅ ⊆ 𝐴
2		eqss 3813	. . 3 ⊢ (𝐴 = ∅ ↔ (𝐴 ⊆ ∅ ∧ ∅ ⊆ 𝐴))
3	1, 2	mpbiran2 702	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 ⊆ ∅)
4	3	bicomi 216	1 ⊢ (𝐴 ⊆ ∅ ↔ 𝐴 = ∅)

Syntax hints:   ↔ wb 198   = wceq 1653   ⊆ wss 3769  ∅c0 4115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-v 3387  df-dif 3772  df-in 3776  df-ss 3783  df-nul 4116

This theorem is referenced by:  ss0  4170  un00  4207  pw0  4531  al0ssb  4985  fnsuppeq0  7561  cnfcom2lem  8848  card0  9070  kmlem5  9264  cf0  9361  fin1a2lem12  9521  mreexexlem3d  16621  efgval  18443  ppttop  21140  0nnei  21245  disjunsn  29924  isarchi  30252  filnetlem4  32888  coss0  34723  pnonsingN  35954  osumcllem4N  35980  resnonrel  38681  ntrneicls11  39170  ntrneikb  39174  sprsymrelfvlem  42539