Theorem ss0b 4341

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

Syntax hints:   ↔ wb 206   = wceq 1542   ⊆ wss 3889  ∅c0 4273

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-dif 3892  df-ss 3906  df-nul 4274

This theorem is referenced by:  ss0  4342  un00  4385  pw0  4755  al0ssb  5243  fnsuppeq0  8142  cnfcom2lem  9622  card0  9882  kmlem5  10077  cf0  10173  fin1a2lem12  10333  mreexexlem3d  17612  efgval  19692  ppttop  22972  0nnei  23077  bdayfinbndlem2  28460  disjunsn  32664  isarchi  33243  filnetlem4  36563  bj-pw0ALT  37356  coss0  38890  pnonsingN  40379  osumcllem4N  40405  resnonrel  44019  ntrneicls11  44517  ntrneikb  44521  sprsymrelfvlem  47950  isubgr0uhgr  48349  iuneq0  49294