Theorem ss0 3465

Description: Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.)

Assertion

Ref	Expression
ss0	|- ( A C_ (/) -> A = (/) )

Proof of Theorem ss0

Step	Hyp	Ref	Expression
1		ss0b 3464	. 2 |- ( A C_ (/) <-> A = (/) )
2	1	biimpi 120	1 |- ( A C_ (/) -> A = (/) )

Syntax hints:   -> wi 4   = wceq 1353   C_ wss 3131   (/)c0 3424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-dif 3133  df-in 3137  df-ss 3144  df-nul 3425

This theorem is referenced by:  sseq0  3466  abf  3468  eq0rdv  3469  ssdisj  3481  0dif  3496  poirr2  5023  iotanul  5195  f00  5409  map0b  6689  phplem2  6855  php5dom  6865  sbthlem7  6964  fi0  6976  casefun  7086  caseinj  7090  djufun  7105  djuinj  7107  nnnninfeq  7128  exmidomni  7142  ixxdisj  9905  icodisj  9994  ioodisj  9995  uzdisj  10095  nn0disj  10140  fsum2dlemstep  11444  fprodssdc  11600  fprod2dlemstep  11632  ntrcls0  13716