Theorem ss0b 4349

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

Syntax hints:   ↔ wb 208   = wceq 1531   ⊆ wss 3934  ∅c0 4289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-dif 3937  df-in 3941  df-ss 3950  df-nul 4290

This theorem is referenced by:  ss0  4350  un00  4392  pw0  4737  al0ssb  5203  fnsuppeq0  7850  cnfcom2lem  9156  card0  9379  kmlem5  9572  cf0  9665  fin1a2lem12  9825  mreexexlem3d  16909  efgval  18835  ppttop  21607  0nnei  21712  disjunsn  30336  isarchi  30804  filnetlem4  33722  coss0  35711  pnonsingN  37061  osumcllem4N  37087  resnonrel  39942  ntrneicls11  40430  ntrneikb  40434  sprsymrelfvlem  43642