Theorem ss0b 3815

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 3814	. . 3
2		eqss 3518	. . 3
3	1, 2	mpbiran2 919	. 2
4	3	bicomi 202	1

Syntax hints:  <->wb 184  =wceq 1395  C_wss 3475  c0 3784

This theorem is referenced by:  ss0  3816  un00  3862  ssdisj  3876  pw0  4177  fnsuppeq0OLD  6132  fnsuppeq0  6947  cnfcom2lem  8166  cnfcom2lemOLD  8174  card0  8360  kmlem5  8555  cf0  8652  fin1a2lem12  8812  mreexexlem3d  15043  efgval  16735  ppttop  19508  0nnei  19613  disjunsn  27453  isarchi  27726  filnetlem4  30199  pnonsingN  35657  osumcllem4N  35683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785